slice - 了解 Frame-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 ，那么非零值可以表示为一个区间，但是值分析插件不能表示“所有类型int的值”除了 0”。

如果你愿意改变前置条件，你可以把它写成一个更容易被值(value)分析插件理解的形式(连同值(value)分析选项 -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;
}