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

【问题标题】：Testing intermediate variables in a large file using Frama-c使用 Frama-c 测试大文件中的中间变量
【发布时间】：2018-09-24 14:11:37
【问题描述】：

我正在尝试使用 Frama-c 来检查我拥有的 C 函数的一些属性。该函数非常大，我需要检查一些中间变量。（我在关注this和this手册）

我的程序结构如下：

整个程序共有 15 条返回语句。

我需要检查的变量在程序中的多个位置被赋值，具体取决于程序的路径。

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 种方法。

只要如上所述设置 var 1，就使用断言。

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

在开头使用注释。

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

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

问题：如何检查属性是否存在中间问题？有示例程序吗？

*我没有包含我的原始函数，因为它很长。

【问题讨论】：

你的问题不清楚。首先，如果您告诉我们您打算进行哪种分析，将会有所帮助。鉴于您提供了指向 WP 插件手册的链接，我可以想象它是您想要使用的那个，在问题中明确说明会更好。其次，您提供的代码不是有效的 C 代码（例如，intermediate var 1 不是变量声明。int var_1 是）。您应该提供mcve，这将有助于我们提供准确的答案（类似“Frama-C 返回错误”：您应该更具体）。
“问题在于 Frama-C 只检查第一个断言”。描述与 Frama-C 的预期行为不符，所以这里恐怕有一些不清楚的地方。正如@Virgile 所提到的，尝试生成一个小的可执行示例应该有助于澄清它。在大多数情况下，如果不能完全解决问题，简单地尝试在一个小案例中重现问题将导致更好地理解问题。如果你想要 Frama-C/WP 的使用示例，优秀的 ACSL by example 应该提供很多。

标签： c frama-c

【解决方案1】：

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

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 三元组的概念，在这个场景中，您通过断言对某个属性的要求（前置条件）来检查（断言）某个属性，并在执行相应的语句后检查该属性是否成立。

希望这会有所帮助。

【讨论】：