使用Frama-C验证max函数时遇alt-ergo未在why3.conf中找到错误

别担心，你遇到的这两个问题都有明确的解决路径，咱们一步步来梳理：

你的代码与报错回顾 #

待验证的max函数 #

/*@ ensures \result >= x && \result >= y; 
    ensures \result == x || \result == y; */ 
int max( int x, int y){ 
    return (x>y) ? x : y; 
}

执行frama-c -wp fct.c后的报错 #

[kernel] Parsing fct.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] Goal typed_max_ensures : not tried
[wp] Goal typed_max_ensures_2 : not tried
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.

1. 修复Alt-Ergo未被Why3识别的问题 #

这个错误的核心是：Why3的配置文件why3.conf里没有记录Alt-Ergo的位置，导致WP插件找不到它。按以下步骤操作：

• 先确认Alt-Ergo安装正常：在终端输入alt-ergo --version，如果能输出类似Alt-Ergo version 2.5.2的版本信息，说明安装没问题；如果没输出，重新用OPAM安装：opam install alt-ergo。
• 更新Why3的Prover配置：执行why3 config --detect，这个命令会自动扫描系统里已安装的证明器，把Alt-Ergo的信息添加到why3.conf中。
• 验证配置生效：运行why3 provers，在输出列表里找到Alt-Ergo，确保它的状态是available。

2. 处理RTE警告（可选但推荐） #

WP提示的Missing RTE guards是指没有启用运行时错误检查的防护逻辑。如果你想验证max函数不会出现整数溢出这类问题，可以在命令里加-wp-rte选项，让WP自动生成并验证相关的运行时安全注解；如果只是想验证你写的两个ensures条件，这个警告不会阻碍验证，但加上-wp-rte会让验证更严谨。

3. 重新运行验证 #

完成上述步骤后，执行以下命令重新验证：

frama-c -wp -wp-prover alt-ergo fct.c

这里-wp-prover alt-ergo明确指定用Alt-Ergo作为证明器，你也可以省略这个参数，让WP自动选可用的证明器。

如果一切正常，你会看到成功的输出：

[kernel] Parsing fct.c (with preprocessing)
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_ensures (QED)
[wp] [Alt-Ergo] Goal typed_max_ensures_2 (QED)
[wp] Proved goals: 2/2

内容的提问来源于stack exchange，提问作者I. Ali