在 FramaC 中假设语句建模

Question

我想使用 Frama-C（Neon 版本）的价值分析 插件的用户断言，但是我在想出合适的[=11 模型时遇到了一些问题=] 语句，这对我应用特定约束非常有用，例如，这是我的测试代码：

#include "/usr/local/share/frama-c/builtin.h"

int main(void)
{
    int selection = Frama_C_interval(0,10);
    int a;
    assume(selection > 5);
    if (selection > 5)
    {
        a = 2;
    }
    else
    {
        a = 1;
    }
    //@ assert a == 2;
    return 0;
}

我希望 selection 的值在此 assume 语句之后大于 5，以便断言有效。我最初的尝试是写这个函数 void assume(int a){ while(!a); return;} ，但没有成功。请帮助我，谢谢。

Answer 1

约束 selection 的最简单方法是使用 assert（当然不会被 Value 证明）。如果要区分实际上是假设的assert和要验证的assert，可以使用ACSL的命名机制，比如

//@ assert assumption: selection > 5;

并验证唯一 assert 未知的是名为 assumption 的那些。

使用 assume 函数不能这样工作，因为它只会将 a 参数的可能值减少为非零。 Value 无法推断 assume 中 a 的值与 main 中 selection 的值之间的关系。但是，有可能帮助它一点点。首先，-slevel 允许并行传播多个抽象状态。其次，在析取式中给出的 assert 将强制 Value 拆分其状态（如果 -slevel 足够大可以这样做）。因此，使用以下代码

#include "builtin.h"

void assume(int a) { while(!a); return; }

int main(void)
{
     int selection = Frama_C_interval(0,10);
     int a;
     /*@ assert selection > 5 || selection <= 5; */
     assume(selection > 5);
    if (selection > 5)
    {
        a = 2;
    }
    else
    {
        a = 1;
    }
    //@ assert a == 2;
    return 0;
}

和以下命令行：

frama-c -cpp-extra-args="-I$(frama-c -print-share-path)" -val -slevel 2

在第一个 assert（显然有效）之后，Frama-C 将分别传播两种状态：一种是 selection > 5，另一种是 selection <= 5。在第一种情况下，assume 以 1 作为参数被调用，因此立即 returns，并且采用 if 的 then 分支，因此第二个 assert 有效。在第二种状态下，assume 被调用为 0，而不是 returns。因此对于控制到达第二个 assert 的所有情况，它都是有效的。

请注意，您确实需要在 main 的正文中添加第一个 assert，并在 ACSL 中复制您传递给 assume 的参数。否则，状态分裂不会发生（更准确地说，你将在 a 上分裂，而不是在 selection 上分裂）。

在 FramaC 中假设语句建模

assume statement modelling in FramaC

frama-c