frama-c - 为什么 Frama-c 的 Eva 插件在实际找到断言的反例时返回未知

Question

我正在尝试在函数中插入断言。这是我所做的:

void foo(int a) {
    //@ assert a == 1;
}

void main() {
   foo(1);
   foo(2);
}

我期望得到一个无效的结果，但 Frama-C 返回一个未知的结果，同时它可以提供调用堆栈的反例。

这是我使用 Frama-C 运行示例时的屏幕截图:

Answer 1

Eva 表示状态未知，因为它观察到一个调用堆栈，其中断言有效，而另一个调用堆栈则无效。但是，由于插件执行过度近似(好吧，不是在这里，因为您的程序很简单，但在一般情况下会出现)，因此它无法确保这两种情况都可以在具体执行中发生:一由于 Eva 使用的抽象无法达到的条件，分支的分支(验证断言的分支或使其无效的分支)可能无法在具体世界中到达。因此，唯一合理的可能性(包含所有可能性)就是在此处设置未知状态。

如果您注释掉 foo(1) 调用，您也会发现出现同样的问题。然后，Eva 会报告该断言无效，但前提是确实可以达到。

最后，这种注释确实是您通常想要首先研究的注释(而不是具有“普通”未知状态的注释)，并且在较新版本的 Frama-C 中(从 v17.0 开始)，您还有一个附加面板Red Alarms，其中列出了至少对一个调用堆栈无效的属性。