使用 Frama-c 测试大文件中的中间变量

Question

我正在尝试使用Frama-c来检查我拥有的C函数的某些属性。该函数非常大，我需要检查一些中间变量。(我正在遵循此手册和本手册(

我的程序具有以下结构：

1. 整个计划中分布着 15 个返回声明。

2. 我需要检查的变量在程序中的多个位置分配了值，具体取决于程序的路径。

   my_function(){
   intermediate var 1=xx;
   //@assert var 1>some_value;
   intermediate var 2=yy;
   return var 4;
   intermediate var 1=xx;
   //@assert var 1>some_value;
   return var 4;
   intermediate var 2=xx;            
   intermediate var 1=yy;
   //@assert var 1>some_value;
   return var 4;
   }
   

说明：我需要检查与 var 1、var 2 和 var 4 相关的某些属性。我尝试了 2 种方法。

1. 每当按上述方式设置 var 1 时，请使用断言。

问题在于 Frama-C 只检查第一个断言。

2. 在开头使用注释。

   /*@ requires valid(var 1);
   ensures var 1 > some_value;
   */
   

在这种情况下，Frama-C 返回错误。

问：如何检查中间问题的属性？有示例程序吗？

*我没有包括我的原始功能，因为它很长。

Answer 1

正如 Virgile 所提到的，你的问题不是很清楚，但我假设你正在尝试验证 var1 和 var2 的一些属性。 这本书提供了一些很好的例子，我认为以下内容应该对你有所帮助。

int abs(int val){
int res;
if(val < 0){
//@ assert val < 0 ;
res = - val;
//@ assert at(val, Pre) >= 0 ==> res == val && at(val, Pre) < 0 ==> res == -val;
} else {
//@ assert !(val < 0) ;
res = val;
//@ assert at(val, Pre) >= 0 ==> res == val && at(val, Pre) < 0 ==> res == -val;
}    
return res;
}

作者在此场景中使用了 Hoare 三元组的概念，在该场景中，您可以通过断言某个属性对属性的要求(前提条件(来检查(断言(某个属性，并在执行相应的语句后检查属性是否成立。

希望这有帮助。