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

Question

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

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

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

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

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

Answer 1

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

如果您注释掉 foo(1) 调用，您也会看到同样的问题。然后eva会报断言无效，但只是前提是确实可以达到.

最后，这种注释确实是您通常首先要研究的注释（与 "plain" 未知状态的注释相反），并且在较新版本的 Frama-C 中（从 v17 开始） .0)，您有一个额外的面板 Red Alarms，其中列出了至少对一个调用堆栈无效的属性。

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

Why Eva plugin of Frama-c return unkown when it acctually found a counter example of an assertion

frama-c