WP does not solve goals with Alt-Ergo
Hi, I am trying to build Frama-C/WP from source and run the test suite (via the bin/test.sh
script and the instructions in https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/wp/tests/README.md). It appears that for every goal that is expected to be solved using Alt-Ergo, WP instead tries (and fails) to solve it with QED alone (example output from bin/test.sh src/plugins/wp/tests
shown below):
File "src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle", line 1, characters 0-0:
diff --git a/_build/default/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/_build/default/src/plugins/wp/tests/wp_plugin/result_qualif/init_const_guard.res.log
index 835fde060..ae2ec7f02 100644
--- a/_build/default/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
+++ b/_build/default/src/plugins/wp/tests/wp_plugin/result_qualif/init_const_guard.res.log
@@ -8,20 +8,20 @@
[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
[wp] 7 goals scheduled
[wp] [Valid] typed_f_ensures_Const (Qed)
-[wp] [Valid] typed_f_ensures_Pointed_Valid (Alt-Ergo) (Cached)
+[wp] [NoResult] typed_f_ensures_Pointed_Valid (Qed)
[wp] [Valid] typed_f_ensures_Q_ReadOnly (Qed)
[wp] [Valid] typed_f_ensures_Q_NotWrite (Qed)
[wp] [Valid] typed_g_ensures_P_not_Const (Qed)
-[wp] [Valid] typed_g_assert_Read (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_g_assert_Guard_against_Const (Alt-Ergo) (Cached)
-[wp] Proved goals: 10 / 11
+[wp] [NoResult] typed_g_assert_Read (Qed)
+[wp] [NoResult] typed_g_assert_Guard_against_Const (Qed)
+[wp] Proved goals: 8 / 11
Terminating: 2
Unreachable: 2
Qed: 4
- Alt-Ergo: 2
- Unsuccess: 1
+ Unsuccess: 3
+ Missing: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f 3 1 4 100%
- g 1 1 3 66.7%
+ f 3 - 4 75.0%
+ g 1 - 3 33.3%
------------------------------------------------------------
I am using the master branch of Frama-C along with OCaml 4.14, Why3 1.7.1, Alt-Ergo 2.4.3 (following #2686 (closed)) - both installed from opam. I am on Linux Mint 20.
Why3/Frama-C seem to identify all the provers I have: bin/frama-c -wp-detect
gives output
[wp] Prover Alt-Ergo 2.4.3 [alt-ergo|altergo|Alt-Ergo:2.4.3]
[wp] Prover Alt-Ergo 2.4.3 [alt-ergo-fpa|Alt-Ergo:2.4.3:FPA]
[wp] Prover CVC4 1.8 [cvc4|CVC4:1.8]
[wp] Prover CVC4 1.8 [cvc4-ce|CVC4:1.8:counterexamples]
[wp] Prover CVC4 1.8 [cvc4-strings|CVC4:1.8:strings]
[wp] Prover CVC4 1.8 [cvc4-strings-ce|CVC4:1.8:strings+counterexamples]
[wp] Prover CVC5 1.0.8 [cvc5|CVC5:1.0.8]
[wp] Prover CVC5 1.0.8 [cvc5-ce|CVC5:1.0.8:counterexamples]
[wp] Prover CVC5 1.0.8 [cvc5-strings|CVC5:1.0.8:strings]
[wp] Prover CVC5 1.0.8 [cvc5-strings-ce|CVC5:1.0.8:strings+counterexamples]
[wp] Prover Z3 4.12.2 [z3|Z3:4.12.2]
[wp] Prover Z3 4.12.2 [z3-ce|Z3:4.12.2:counterexamples]
[wp] Prover Z3 4.12.2 [z3-nobv|Z3:4.12.2:noBV]
How can I fix this and get the test suite to run successfully? Thanks