Frama-C WP插件为何对main与重命名函数的断言验证结果不同

算力阿峰

2026-8-27

问题背景

以下为最小可复现代码（修改自Frama-C权威教程3.2.3.3节「副作用」部分）：

int h = 42;

/*@
  requires \valid(a) && \valid(b);
  requires \valid_read(a) && \valid_read(b);
  ensures *a == \old(*b) && *b == \old(*a);
 */
void swap( int *a, int *b) {
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

int main(void) {
    int a = 37;
    int b = 91;

    //@ assert h == 42;
    swap(&a, &b);
    //@ assert h == 42;
  return 0;
}

验证观测到的现象：

当指定WP插件验证目标为main函数时，可成功证明swap调用前的//@ assert h == 42;断言成立
仅将代码中main函数重命名为test_swap，指定WP验证目标为test_swap时，同位置的同一条断言无法被证明
两次验证操作均仅指定单个目标函数，使用的Frama-C版本为25.0-beta (Manganese)
多数使用者可理解EVA插件对main函数的特殊处理逻辑，但通常会默认WP作为模块化验证工具对所有函数一视同仁，因此该现象容易引发困惑

底层技术原因

WP采用模块化验证逻辑：对普通待验证函数，仅以函数显式标注的requires子句作为入口状态的全部约束，不会对函数的调用上下文做额外假设，默认函数可能在程序运行的任意阶段被任意代码调用。
这套逻辑唯一的特例是名为main的函数：

Frama-C默认将main识别为C程序的标准入口点，根据C语言规范，进入main函数前没有用户代码执行，所有静态存储期对象（全局变量、文件作用域静态变量、函数内静态变量）均保持其定义时的初始化值
因此WP会为main函数自动补充隐式前置条件：所有静态存储期对象的值等于其初始化值，无需用户手动在requires中写明

示例中全局变量h定义时初始化为42，验证main时，隐式前置条件直接保证函数入口处h == 42，位于swap调用前的第一条断言自然可以被直接证明，和swap函数的契约逻辑无关。
当函数被重命名为test_swap后，WP将其判定为普通函数，不会补充上述全局变量初始化的隐式前置条件：WP会认为该函数被调用前，其他代码完全可能修改过全局变量h的值，入口处h的取值没有任何约束，因此无法证明h == 42的断言。

若需要让非main函数获得与main一致的入口状态假设，可行的操作方式包括：

手动为非main函数添加显式前置条件，明确约束全局变量的入口值：//@ requires h == 42;
启动Frama-C时添加-main <函数名>参数，显式指定对应函数为程序入口点，WP会为其自动补充静态存储期对象符合初始化值的隐式前置条件，即可复现验证main时的行为，成功证明对应断言。

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