Frama-C验证失败咨询：无符号整数代码为何无法通过验证？

核心问题在于ACSL规范的表达式语义与C语言无符号整数运算语义的差异：

• ACSL（Frama-C使用的规范语言）中的表达式采用数学整数语义：requires里的y + 1 >= 1024是指数学上的y+1值大于等于1024，不存在溢出概念——哪怕y是无符号整数类型的最大值UINT_MAX，数学上UINT_MAX + 1也是一个远大于1024的数，满足该前置条件。
• 但C语言中的无符号整数加法遵循**模2^{N语义**（N是无符号类型的位数，比如32位就是2}32）：当y取UINT_MAX时，y + 1会溢出，结果为0。此时代码中y = y + 1执行后，y的值是0，显然不满足断言y >= 1024。

Frama-C的WP插件会严格遵循C语言的语义规则，因此它会认定存在满足前置条件但不满足断言的场景（即y=UINT_MAX时），导致断言无法被证明。

而有符号整数版本能通过验证的原因是：C语言中有符号整数溢出属于未定义行为，WP插件默认会假设有符号整数运算不会发生溢出。此时前置条件y + 1 >= 1024（数学语义）结合无溢出假设，代码中的y + 1结果与数学上的y+1完全一致，因此y >= 1024必然成立。

修复方案 #

如果要让无符号版本通过验证，可选择以下两种方式：

1. 修改前置条件，明确排除溢出场景：

/*@ requires (x != 0) && y < UINT_MAX && (y + 1 >= 1024);
*/

2. 使用ACSL内置函数表示C风格的无符号加法，让前置条件与代码行为一致：

/*@ requires (x != 0) && @\unsigned_add(y, 1) >= 1024;
*/

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