frama-c - 用户错误 : Prover 'alt-ergo' not found in why3. conf

Question

我正在尝试使用 Frama-c 测试一个函数:

/*@
    ensures \result >= x && \result >= y;
    ensures \result == x || \result == y;
*/

int max( int x, int y){
    return (x>y) ? x : y;
}   

在我安装了所有要求之后:OPAM、why3、alt-ergo
每当我执行 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.

Answer 1

如 Frama-C's installation instructions 中所述, why3必须明确配置为检查可用的证明者，通过 why3 config --detect命令(请注意，根据您安装的 Why3 的​​确切版本，您也可以使用 why3 config --full-config 代替)。您应该看到如下输出:

Found prover Alt-Ergo version 2.0.0, OK.
... possibly other provers if you have installed them
Save config to /PATH/TO/HOME/.why3.conf

之后，您将能够在 Frama-C/WP 中使用证明程序