WP插件：为什么下面的简化代码验证失败

Question

我是一位新的 Frama-C 用户，我正在尝试证明一个大型项目的某些属性。我看到一个特定的证明失败了，并尝试将问题减少到最小的可重现示例，以下是代码：

#include <stdlib.h>

/*@ requires (x != 0) && (y + 1 >= 1024);
*/
int f1(unsigned int x, unsigned int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

我使用以下命令来验证：

frama-c -wp -wp-prover=alt-ergo,z3,cvc4 a.c -kernel-warn-key annot-error=active -then -no-unicode -report

上述代码无法通过 frama-c 进行验证，并显示以下消息：

Assertion x != 0 && y >= 1024: Unproven

您能否解释一下为什么此验证失败？

我尝试手动简化原始证明并提出了上面的例子。我希望验证能够通过。我相信我可能误解了 frama-c 如何对待 C 数据类型的“y+1”，而不是像 Int 这样的纯数学数据类型。

编辑：

以下代码验证成功（我只是将变量类型从无符号更改为有符号）：

#include <stdlib.h>

/*@ requires (x != 0) && (y + 1 >= 1024);
*/
int f1(int x, int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

编辑2： 版本： Frama-C：27.1（钴） 另类：2.4.3 CVC4：1.6 Z3：4.12.2

编辑3：

我也在frama-c 28.1版本中尝试过，但仍然失败。

Answer 1

主要问题是 ACSL 中的

y + 1

与 C 中的

y+1

的含义不同。更准确地说，正如 ACSL 手册 中提到的，算术运算在 ACSL 中是通过数学、无界整数进行评估的。因此，

y+1>=1024

子句中的

requires

不足以得出作业中

y>=1024

之后的

y=y+1

的结论：如果我们将

UINT_MAX

传递给

f

，我们最终会得到

y == 0

。添加另一个

requires

，例如

y+1 <= UINT_MAX + 1

，将解决问题。

关于

int

的变体，情况有些不同。事实上，虽然 unsigned 溢出在 C 中被完美定义（我们只是包装该值），但 signed 溢出却不是：结果是实现定义的，并且可能会引发信号。因此，默认情况下 Frama-C 会认为有符号溢出是运行时错误。对于 Wp，这意味着它将假设不会发生此类溢出，并使用

-wp-rte

检查委托给 Rte 插件生成注释：使用此选项，您将获得未经证明的断言，即由 Rte 生成的。

类似地，如果将选项

-warn-unsigned-overflow

添加到

unsigned

变体，一切似乎一开始都被证明了，但是添加

-wp-rte

揭示了未经证明的、Rte 生成的断言，而将选项

-no-warn-signed-overflow

添加到

signed

变体为您提供与

unsigned

相同的行为。

总而言之，如果我们使用以下 C 文件

t.c

并使用各种选项集启动

frama-c

，我们将获得以下结果：

#include<limits.h>

/*@ requires (x != 0) && (y + 1 >= 1024);
#ifdef ACSL_NO_OVERFLOW
  requires no_overflow: y + 1 <= UINT_MAX;
#endif
*/
int f1(unsigned int x, unsigned int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

/*@ requires (x != 0) && (y + 1 >= 1024);
#ifdef ACSL_NO_OVERFLOW
  requires no_overflow: y + 1 <= INT_MAX;
#endif
*/
int f2(int x, int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

frama-c命令	已证实的目标
frama-c -wp t.c	5/6
frama-c -wp t.c -wp-rte	5/7
frama-c -wp t.c -wp-rte -cpp-extra-args =“-DACSL_NO_OVERFLOW”	7/7
frama-c -wp t.c -警告无符号溢出	6/6
frama-c -wp t.c -警告无符号溢出-wp-rte	6/8
frama-c -wp t.c -无警告签名溢出	4/6
frama-c -wp t.c -无警告签名溢出-wp-rte	4/6
frama-c -wp t.c -warn-unsigned-overflow -wp-rte -cpp-extra-args =“-DACSL_NO_OVERFLOW”	8/8
frama-c -wp t.c -no-warn-signed-overflow -wp-rte -cpp-extra-args =“-DACSL_NO_OVERFLOW”	6/6