Frama-c WP 和先决条件

Question

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

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

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

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

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

Answer 1

作为初步，让我明确一点，对于“How/When Frama-C 是否证明先决条件”的问题没有明确的答案。更准确地说，这在很大程度上取决于您使用的插件。既然你提到了WP，我就重点说一下。

在一般情况下，函数 f 的前提条件应该在每个调用点都成立（这就是函数契约概念的来源：f 保证 post-条件成立时 returns 仅适用于可以保证调用前前提条件成立的调用者）。因此，如果您在选择证明的函数中没有调用 f，则不会尝试证明先决条件。

现在，main 函数（或更准确地说是 Frama-C 的 -main 选项指定的函数，默认为 main）有一个例外，因为它应该是程序的入口点，并且通常不会在其他任何地方调用，尝试检查初始程序状态（其中所有全局变量都等于它们的初始值，形式可以有任何值）遵守前提。请注意，选项 -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 file.c

仅提供 1 个

Frama-c WP 和先决条件

Frama-c WP and preconditions

static-analysis

frama-c