4

我想知道是否可以使用 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 ...”

4

2 回答 2

4

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

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

如果你愿意改变前置条件，你可以写成更容易被价值分析插件理解的形式（连同价值分析选项-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;
}
于 2013-07-10T17:25:56.527 回答
2

这与您的主要问题没有任何关系，但是您的ensures a == \old(a)条款没有达到您的预期。如果你使用 option 漂亮地打印你的源代码-print，你会看到它已经被默默地转换为ensures \old(a) == \old(a).

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

于 2013-07-10T20:50:30.560 回答