Frama-C 28.1无法证明无符号加法溢出性质，求排查方案

问题背景 #

刚安装Frama-C 28.1（Nickel），默认配置下无法证明无符号加法相关性质。编写了包含行为规范的file.c代码：

#include <limits.h>

/*@ 
  @ assigns \nothing;
  @ 
  @ behavior wont_overflow:
  @   assumes x + y <= UINT_MAX;
  @   ensures \result == (x + y) % (UINT_MAX + 1); // TODO: it's general ensure
  @   ensures \result >= x;
  @
  @ behavior will_overflow:
  @   assumes x + y > UINT_MAX;
  @   ensures \result == (x + y) % (UINT_MAX + 1); // TODO: it's general ensure
  @   ensures \result < x;
  @
  @ complete behaviors wont_overflow, will_overflow;
  @ disjoint behaviors wont_overflow, will_overflow;
  @*/
unsigned uAdd(unsigned x, unsigned y) {
    return x + y;
}

运行命令：

frama-c -wp -wp-rte -rte file.c

输出显示will_overflow行为的两个ensure语句验证超时：

[kernel] Parsing file.c (with preprocessing)
[rte:annot] annotating function uAdd
[wp] 7 goals scheduled
[wp] [Timeout] typed_uAdd_will_overflow_ensures_2 (Qed 0.70ms) (Alt-Ergo)
[wp] [Timeout] typed_uAdd_will_overflow_ensures (Qed 0.72ms) (Alt-Ergo)
[wp] Proved goals:    7 / 9
  Terminating:       1
  Unreachable:       1
  Qed:               3
  Alt-Ergo 2.5.3:    2 (9ms-12ms)
  Timeout:           2

疑问：问题根源是什么？是否与CLI参数有关？

问题分析与解决 #

根源定位 #

不是CLI参数的问题，核心原因在于：

• 无符号加法的溢出语义需要结合模运算的数论性质证明，Alt-Ergo默认配置下对这类复杂数论推理的效率不足，导致超时。
• 规范中直接使用(x + y) % (UINT_MAX + 1)的表述，要求求解器关联“C无符号加法自动模UINT_MAX+1”与显式模运算的等价性，这需要展开大量数论规则，尤其是在溢出假设x + y > UINT_MAX下，推导result < x这类结论的推理链较长，超出了Alt-Ergo默认超时时间内的处理能力。

解决方法 #

1. 增加求解器超时时间
   给Alt-Ergo设置更长的超时阈值，比如30秒：

   frama-c -wp -wp-rte -rte -wp-timeout 30 file.c
   

   让求解器有足够时间完成数论推理。

2. 简化规范表述
   利用C标准中无符号加法本身就是模UINT_MAX+1运算的语义，将规范中的\result == (x + y) % (UINT_MAX + 1)替换为\result == x + y，WP会直接识别这一内置语义，减少求解器的推理负担：

   /*@ 
     @ assigns \nothing;
     @ 
     @ behavior wont_overflow:
     @   assumes x + y <= UINT_MAX;
     @   ensures \result == x + y;
     @   ensures \result >= x;
     @
     @ behavior will_overflow:
     @   assumes x + y > UINT_MAX;
     @   ensures \result == x + y;
     @   ensures \result < x;
     @
     @ complete behaviors wont_overflow, will_overflow;
     @ disjoint behaviors wont_overflow, will_overflow;
     @*/
   

3. 切换更高效的求解器
   如果已安装Z3，它对模运算和数论推理的效率通常优于Alt-Ergo，使用以下命令验证：

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

内容的提问来源于stack exchange，提问作者Miroslav