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.