Frama-c WP 和前提条件

编程问答 2022-05-16

问题描述

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

  1. Frama-c 如何证明先决条件？
  2. Frama-c 什么时候尝试证明先决条件？

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

enter image description here

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

enter image description here

我假设 main 函数对此有影响，但它是全貌吗？只有当函数是 main 时，前提条件才可以证明吗？

解决方法

作为初步，让我明确一下，“Frama-C 如何/何时证明先决条件”的问题没有明确的答案。更准确地说，这高度依赖于您使用的插件。既然你提到了WP，那我就重点说一下。

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

现在，main 函数（或更准确地说是由 Frama-C 的 -main 选项指定的函数，默认为 main）有一个例外，正如它所假设的作为程序的入口点，并且通常不会在其他任何地方调用，尝试检查初始程序状态（其中所有全局变量都等于它们的初始值，并且形式可以具有任何值）是否遵守前提条件。请注意，选项 -lib-entry 表示全局变量具有初始值的假设不应该成立，在这种情况下，WP 将不会尝试证明 main 函数的前提条件，因为它无法做出任何假设关于它的调用上下文。例如，以下代码：

int X = 1;

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

将给出 2 个（有效）证明义务与 frama-c -wp -main f file.c，只有 1 个与 frama-c -wp -main f -libentry file.c

frama-cstatic-analysis