Frama-C WP Tutorial | 函数契约

h-jr.me

Tinymist 的 Typst 无用声明检测一路顺风经验贴｜末九17%上岸南大计院 SOP 和 POS Verilog 打砖块游戏 Verilog 基础语法 Wasm 二进制结构我和 Typst 的 2024 计算机网络 TCP 大实验 2024 年冬天吃的第一个亏从换电脑开始我学编程原神 Rust 记三天数模国赛 C 编译体系

2025-07-06 · via h-jr.me

由霍尔逻辑，霍尔三元组可以定义为

{P}C{Q}\{P\} C \{Q\}

其中 PP 和 QQ 是谓词，即在特定程序点上表达内存属性的逻辑公式。CC 是定义程序的一系列指令。

函数契约的目标是说明函数期望的输入属性，以及作为交换，输出将得到保证的属性。函数的期望输入称为前置条件，输出的属性称为后置条件。契约用 ACSL 表达，它和 C 语言长得比较像。

/*@
  //契约
*/
void foo(int bar){
}

注释块开头的 @，向 Frama-C 表明接下来的是注释不是要忽略的注释块。

后置条件

用 ensures 子句引入函数的后置条件。比如函数 abs()：

/*@
  ensures \result >= 0;
*/
int abs(int val){
  if (val < 0){
    return -val;
  }
  return val;
}

\result 是一个特殊的变量，表示函数的返回值。上面的后置条件表明，函数的返回值总是大于等于 0。显然这个条件很宽泛，进一步约束函数的一般行为的话，可以继续补充：

/*@
  ensures \result >= 0;
  ensures (val >= 0 ==> \result == val) &&
          (val < 0 ==> \result == -val);
*/
int abs(int val){
  if (val < 0){
    return -val;
  }
  return val;
}

这里出现的 ==> 就是 ⇒\Rightarrow，表示逻辑蕴含。同理，<==> 表示逻辑等价。

我们可以通过给属性命名来减少重复。比如上面的例子可以改写为：

/*@
  ensures positive_value: function_result: \result >= 0;
  ensures (val >= 0 ==> \result == val) &&
          (val < 0 ==> \result == -val);
*/
int abs(int val){
  if (val < 0){
    return -val;
  }
  return val;
}

通过 Frama-C 的 -wp 选项，我们可以检查函数契约是否满足。比如上面的例子可以用下面的命令检查：

输出为：

❯ frama-c -wp abs.c
[kernel] Parsing abs.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] Proved goals:    4 / 4
  Terminating:     1
  Unreachable:     1
  Qed:             2
[wp:pedantic-assigns] abs.c:6: Warning:
  No 'assigns' specification for function 'abs'.
  Callers assumptions might be imprecise.

如果输出中有 Proved goals: 4 / 4，表示所有的目标都被证明了。Terminating: 1 表示函数是终止的，Unreachable: 1 表示有一个不可达的目标。

但这样并不能排除运行时错误（RTE）。比如上面的 abs() 函数没有处理整数溢出的问题。在 Ivette 中可以用以下设置来处理：

rte

然后就能看到 Frama-C 生成了一些运行时错误（RTE）保护代码。比如上面的 abs() 函数会生成以下代码：

/*@ assert rte: signed_overflow: -2147483647 ≤ val; */

但是执行验证时会发现，WP 不能证明这个断言的真伪（橙色），也就是说无法保证整数溢出不会发生。

rte-overflow

对应的，在 cli 中的输出会是：

❯ frama-c -wp -wp-rte abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte:annot] annotating function abs
[wp] 3 goals scheduled
[wp] [Timeout] typed_abs_assert_rte_signed_overflow (Alt-Ergo)
[wp] Proved goals:    4 / 5
  Terminating:     1
  Unreachable:     1
  Qed:             2
  Timeout:         1
[wp:pedantic-assigns] abs.c:6: Warning:
  No 'assigns' specification for function 'abs'.
  Callers assumptions might be imprecise.

说明这个断言无法被证明是因为超时了。

前置条件

前置条件用 requires 子句引入。比如函数 abs() 的前置条件可以是：

#include <limits.h>
/*@
  requires INT_MIN < val;
  ensures \result >= 0;
  ensures (val >= 0 ==> \result == val) &&
          (val < 0 ==> \result == -val);
*/
int abs(int val){
  if (val < 0){
    return -val;
  }
  return val;
}

这时候再运行 frama-c -wp -wp-rte abs.c，会发现所有的目标都被证明了。

❯ frama-c -wp -wp-rte abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte:annot] annotating function abs
[wp] 3 goals scheduled
[wp] Proved goals:    5 / 5
  Terminating:     1
  Unreachable:     1
  Qed:             3
[wp:pedantic-assigns] abs.c:10: Warning:
  No 'assigns' specification for function 'abs'.
  Callers assumptions might be imprecise.

也可以写一个函数契约的测试程序来验证函数契约是否满足。比如：

void foo(int a){
  int b = abs(42);
  int c = abs(-42);
  int d = abs(a);
  int e = abs(INT_MIN);
}

再次验证：

❯ frama-c -wp -wp-rte abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte:annot] annotating function abs
[rte:annot] annotating function foo
[wp] 9 goals scheduled
[wp] [Timeout] typed_foo_call_abs_4_requires (Qed 1ms) (Alt-Ergo)
[wp] [Timeout] typed_foo_call_abs_3_requires (Qed 0.56ms) (Alt-Ergo)
[wp] Proved goals:    9 / 11
  Terminating:     1
  Unreachable:     1
  Qed:             7 (0.56ms-0.21ms-1ms)
  Timeout:         2
[wp:pedantic-assigns] abs.c:10: Warning:
  No 'assigns' specification for function 'abs'.
  Callers assumptions might be imprecise.
[wp:pedantic-assigns] abs.c:17: Warning:
  No 'assigns' specification for function 'foo'.
  Callers assumptions might be imprecise.

此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。原文来自 — 版权归原作者所有。

推荐订阅源

h-jr.me

后置条件

前置条件