Frama-C WP与EVA分析差异及WP-RTE断言证明方法问询

测试用C程序 #

int test(int a) {
    return 10/a;
}

int main() {
    int a = 0;
    test(a);
    return 0;
}

EVA与WP-RTE生成的RTE守卫对比 #

执行以下命令可生成包含RTE守卫的代码：

• 使用EVA：frama-c -eva -print test.c，生成的代码包含断言：

  /*@ assert Eva: division_by_zero: a ≢ 0; */
  

• 使用WP-RTE：frama-c -wp -wp-rte -print test.c，生成的代码包含断言：

  /*@ assert rte: division_by_zero: a ≢ 0; */
  

EVA的检测结果 #

EVA可直接检测到断言违规，输出如下：

[eva:alarm] test.c:2: Warning: division by zero. assert a ≢ 0;
[eva] test.c:2: assertion 'Eva,division_by_zero' got final status invalid.

WP的分析情况 #

• 默认超时（设置超时时间为2秒）：frama-c -wp -wp-rte -wp-timeout 2 test.c
• 将超时时间设为300秒时，结果为：

  [wp] [Unknown] typed_test_assert_rte_division_by_zero (Qed 0.69ms) (Alt-Ergo)
  

• 即使将断言改写为前置条件//@ requires a != 0;，EVA仍能发现其无效，但WP依旧超时或返回结果未知。

问题 #

根据Frama-C Eva手册，EVA生成的证明义务与WP-RTE断言一致，请问两者分析的差异是什么？如何让WP证明WP-RTE断言？

解答 #

两者分析的核心差异 #

1. 分析方法本质不同

   • EVA是抽象解释工具：通过对程序状态进行抽象建模，跟踪变量的可能取值范围，能直接定位具体的违规实例（如本例中a=0的执行路径），属于偏向错误检测的静态分析方法，只要找到一个违反断言的路径就会触发报警。
   • WP是演绎验证工具：基于逻辑推理和定理证明，需要从程序的前置条件、循环不变式等逻辑依据出发，推导断言在所有可能执行路径下都成立。它不会主动寻找反例，当缺乏足够的逻辑链完成证明时，就会返回Unknown或超时。

2. 核心目标不同

   • EVA的目标是检测运行时错误的存在性，聚焦于"是否存在违规路径"；
   • WP的目标是证明断言的普遍性，聚焦于"是否所有路径都满足断言"。

让WP证明WP-RTE断言的方法 #

1. 明确约束条件，暴露矛盾
   在调用test函数前添加明确的断言，将变量的取值约束暴露给WP。比如修改main函数：

   int main() {
       int a = 0;
       /*@ assert a != 0; */ // 明确触发矛盾，WP可直接证明该断言不成立
       test(a);
       return 0;
   }
   

   此时执行frama-c -wp -wp-rte test.c，WP会直接返回该断言的证明失败，从而指出违规。

2. 切换定理证明器
   不同的证明器对整数算术问题的处理效率和能力不同，可尝试使用Z3或CVC4替代默认的Alt-Ergo，命令示例：

   frama-c -wp -wp-rte -wp-prover z3 test.c
   

3. 添加辅助逻辑断言
   对于更复杂的程序，可手动添加中间断言，帮助WP构建完整的推理链，明确变量在关键节点的取值范围或属性。

4. 调整WP分析参数

   • 延长超时时间：使用-wp-timeout <秒数>设置更长的超时阈值；
   • 启用全面分析：添加-wp-full参数让WP进行更深入的分析；
   • 拆分证明义务：使用-wp-split将复杂的证明义务拆分为多个子任务，降低单个证明的复杂度。

内容的提问来源于stack exchange，提问作者Caio Vinícius