static-analysis - Frama-c WP 和先决条件

Question

我有两个关于先决条件和 Frama-c wp 的问题:

1. Frama-c 如何证明前提条件？
2. Frama-c 何时尝试证明先决条件？

我问这些问题是因为有时 frama-c wp 甚至不尝试证明，有时它成功地证明了前提条件，有时它失败了，例如在第一个屏幕截图中没有尝试证明

但在第二个屏幕截图中，我们尝试证明但失败了

我假设主要功能对此有影响，但它是全貌吗？只有当函数是 main 时，前置条件才需要证明吗？

Answer 1

首先，让我明确一点，“Frama-C 如何/何时证明先决条件”这个问题没有明确的答案。更准确地说，这在很大程度上取决于您使用的插件。既然你提到了 WP，那我就重点说说吧。

在一般情况下，函数 f 的前提条件应该在每个调用点都成立(这就是函数契约概念的来源:f 保证当它仅返回到可以保证调用前前提条件成立的调用者时，后置条件成立)。因此，如果您在选择证明的函数中没有对 f 的任何调用，则不会尝试证明先决条件。

现在，main 函数(或者更准确地说是 Frama-C 的 -main 选项指定的函数，默认为 main )，因为它应该是程序的入口点，通常不会在其他任何地方调用，所以会尝试检查初始程序状态(所有全局变量都等于它们的初始值，并且formals 可以有任何值)尊重前提条件。请注意，选项 -lib-entry 表示关于全局变量具有初始值的假设不应该成立，在这种情况下，WP 将不会尝试证明 main 函数，因为它不能对其调用上下文做出任何假设。例如，以下代码:

int X = 1;

/*@ requires X == 1;
    ensures \result == 1;
*/
int f() { return X; }

将对 frama-c -wp -main f file.c 给出 2 个(有效)证明义务，对 frama-c -wp -main f -libentry 文件仅给出 1 个。 c