ACSL 及Frama-C验证工具简介（二）

实例演示

我们已经介绍了 ACSL 和 WP 的基本思想，下面我们将结合实例演示如何使用 WP 来验证包含 ACSL 注释的 C 项目。

示例代码介绍

我们的示例代码围绕寻找数组中最大值的问题展开。这个项目包含三个文件。项目的入口 main 函数在 max_seq_main.c 文件中。该 main 函数调用一个名为 max_seq 的函数计算给定数组中的最大值。此 max_seq 函数的定义位于头文件 max_seq.h 中。而 max_seq 函数的实现则在 max_seq.c 文件中。我们力图通过这种组织方式模拟一个真实项目的结构，max_seq_main.c 文件代表上层逻辑，max_seq.c 代表底层实现，头文件则是接口。三个文件的内容如下：

/* max_seq_main.c */
#include "max_seq.h"

int main() {
    int array[10] = {3, 1, 4, 1, 5, 9, 2, 6, 5, 3};
    int m = max_seq(array, 10);
    //@ assert \exists int i; m == array[i];
    //@ assert \forall int i; 0 <= i < 10 ==> m >= array[i];
    return 0;
}

/* max_seq.h */
/*@ requires n > 0 && \valid(p