问题描述
我正在尝试使用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.
解决方法
如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中的证明