Frama-C 使用“/*@ Ensures”证明 While 循环

Question

我是 Frama-C 的新手，我正在尝试验证 C 代码。该代码非常基本，但不知何故我无法验证它。

\n

总之，我试图证明该函数或循环是否曾经运行过。为此，我在开始时为变量指定了一个值 (4)。在函数中，我将值更改为“5”，并且我尝试确保变量5位于末尾。

\n

代码：

\n

#include <stdio.h>\nint x=4;\n/*@\nensures x ==5;\n*/\nint abs(int val){\n\n    int accept=0;\n    int count=3;\n    /*@\n    loop invariant 0 <= count <= \\at(count, Pre);\n    loop assigns accept,x,count; \n    loop variant count;\n    */\n    while (count !=0){\n        x=5;\n        accept =1;\n        count--;\n    }\n    return x;\n }\n

\n

我向 CLI 发出命令“frama-c-gui -wp -rte testp4.c”来启动 frama-c。

\n

结果：\n Frama-1

\n

但“*@ 确保 x \xe2\x89\xa1 5; */” 仍然未知。

\n

有人可以帮我解决这个问题吗？如果我"x=5;"在 while 循环之外（返回之前）它会验证/*@ ensures x ==5; */

\n

预先感谢所有贡献者！

\n

Answer 1

这里的大多数问题都与内置标签的使用有关。以下是我们需要的标签：

• Pre：前提条件下的状态
• Post：后置条件中的状态
• LoopEntry：开始循环时的状态
• 这里：使用它的程序点的状态

首先要事。我不知道您使用的是哪个版本的 Frama-C，但我建议更新;)。为了防止错误，您将收到以下错误消息：

[kernel:annot-error] file.c:11: Warning: 
  unbound logic variable count. Ignoring loop annotation

为什么？因为你说的是count​​在它不存在的前提下。请注意，在旧版本的 Frama-C 中，WP 可能可以接受这一点，因为在某些情况下，局部变量的预状态和初始化被合并。

我们想要的可能是“当前值count介于 0 和我们开始循环时的值之间”，因此：

loop invariant 0 <= count <= \at(count, LoopEntry);
which is:
loop invariant 0 <= \at(count, Here) <= \at(count, LoopEntry);

现在我们有了这个（经过验证的）不变量，我们希望将循环的行为与后置条件联系起来（当前，我们的循环不变量没有说明任何内容x，并且 WP 不使用循环体。这意味着我们需要另一个不变量，即“当count开始循环时不等于其值时，x为 5`”。

因此：

loop invariant count != \at(count, LoopEntry) ==> x == 5 ;

这允许完全证明该程序:)。最终注释程序：

[kernel:annot-error] file.c:11: Warning: 
  unbound logic variable count. Ignoring loop annotation

关于为什么\at(count, Pre) != 0 ==> \at(x, Post) == 5（在评论中）不起作用的一些话：

• \at(count, Pre)是函数count前置条件中的值，是函数后置条件中的值。因此，这不是我们需要的。\at(count, Post)count