了解 Frama-C 切片器结果

Question

我想知道是否可以使用 Frama-C 进行某种前向条件切片，我正在通过一些示例来了解如何实现这一点。

我有这个简单的例子，它似乎导致了一个不精确的切片，我不明白为什么。这是我要切片的函数：

int f(int a){
int x;
if(a == 0)
    x = 0;
else if(a != 0)
    x = 1;
return x;
}

如果我使用这个规范：

/*@ requires a == 0;
  @ ensures \old(a) == a;
  @ ensures \result == 0;
*/

然后 Frama-C 使用“f -slice-return”标准和 f 作为入口点返回以下切片（精确）：

/*@ ensures \result ≡ 0; */
int f(void){
  int x;
  x = 0;
  return x;
}

但是当使用这个规范时：

/*@ requires a != 0;
  @ ensures \old(a) == a;
  @ ensures \result == 1;
*/

然后所有指令（和注释）仍然存在（当我等待这个切片返回时：

/*@ ensures \result ≡ 1; */
int f(void){
  int x;
  x = 1;
 return x;
}

)

在最后一种情况下，切片是否不精确？在这种情况下，可能是什么原因？

问候，

罗曼

编辑：我写了“else if(a != 0) ...”，但问题仍然存在于“else ...”

Answer 1

在 Frama-C 中，切片插件依赖于称为值分析的初步静态分析插件的结果。

---

这个值分析可以表示变量a 时a == 0 的值（在这种情况下，值的集合是{ 0 }）但是很难表示a 的值，因为已知a != 0。在后一种情况下，如果尚不知道a 是正数还是负数，则值分析插件需要近似a 的值集。如果已知a 为正数，例如如果它是unsigned int，则非零值可以表示为一个区间，但值分析插件不能表示“除0 之外的所有int 类型的值”。

---

如果你愿意改变前置条件，你可以写成更容易被价值分析插件理解的形式（连同价值分析选项-slevel）：

$ cat t.c
/*@ requires a < 0 || a > 0 ;
  @ ensures \old(a) == a;
  @ ensures \result == 0;
*/

int f(int a){
int x;
if(a == 0)
    x = 0;
else if(a != 0)
    x = 1;
return x;
}
$ frama-c -slevel 10 t.c -main f -slice-return f -then-on 'Slicing export' -print 
…
/* Generated by Frama-C */
/*@ ensures \result ≡ 0; */
int f(void)
{
  int x;
  x = 1;
  return x;
}

Answer 2

这与您的主要问题无关，但您的 ensures a == \old(a) 子句没有达到您的预期。如果您使用选项-print 漂亮地打印您的源代码，您会看到它已被默默地转换为ensures \old(a) == \old(a)。

ACSL 语言不允许在 post-state 中引用形式变量的值，主要是因为从调用者的角度来看这是没有意义的。 （调用终止后弹出被调用者的栈帧。）