了解FRAMA-C切片器结果 [英] Understanding Frama-C slicer results

问题描述

我想知道是否有可能使用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 
esult == 0;
*/

然后Frama-C返回以下切片(精确)，使用"f-Slice-Return"标准，以f作为入口点：

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

但在使用此规范时：

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

然后保留所有指令(&；批注)(当我等待返回此切片时：

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

)

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

问候您，

罗曼

编辑：我写了"Else if(a！=0)."但问题仍然是"Else."

推荐答案

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

---

此值分析可以表示变量aWhena == 0的值(本例中的值集为{ 0 })，但在已知a != 0时很难表示a的值。在后一种情况下，如果还不知道a为正或负，则值分析插件需要近似a的值集。如果已知a为正，例如，如果它是一个unsigned int，则非零值可以表示为一个间隔，但是值分析插件不能表示"除0之外的所有int类型的值"。

---

如果您愿意更改前提条件，可以将其写成更容易被价值分析插件理解的形式(连同价值分析选项-slevel)：

$ cat t.c
/*@ requires a < 0 || a > 0 ;
  @ ensures old(a) == a;
  @ ensures 
esult == 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 
esult ≡ 0; */
int f(void)
{
  int x;
  x = 1;
  return x;
}

这篇关于了解FRAMA-C切片器结果的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！