[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL
Steps to reproduce the issue
- Make sure Isabelle/HOL is installed and
why3
is configured to use it. - Create file
test.h
with the following code:
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
- Run WP plugin selecting Isabelle/HOL as a backend:
frama-c -wp -wp-prover=why3:isabelle -wp-interactive=fix -wp-cache=none test.h
Expected behaviour
Earlier versions of Frama-C (e.g. 27.1) produce the following output:
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 0
Isabelle 2022: 1 (8.1s)
with the theory
theory lemma_enumeration_length imports Why3.Why3 begin
why3_open "lemma_enumeration_length.xml"
why3_vc wp_goal
using assms L_enumeration_def
by (induction i) (simp_all add: facts.length_concat length_cons length_nil)
why3_end
end
Actual behaviour
Frama-C 28.0 produces the following:
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failure] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Failed: 1
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 28.0 (Nickel)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04.4 LTS
Additional information (optional)
-wp-msg-key why3_api
gives the following error trace:
[wp] Failure: [Why3 Error] anomaly: Sys_error(".../.frama-c/wp/interactive/lemma_enumeration_length/.xml: No such file or directory")
Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
Called from Frama_c_kernel__Command.pp_to_file in file "src/libraries/utils/command.ml", line 31, characters 13-35
Called from Wp__ProverWhy3.prepare in file "src/plugins/wp/ProverWhy3.ml", line 1339, characters 6-130
Called from Wp__ProverWhy3.interactive in file "src/plugins/wp/ProverWhy3.ml", line 1352, characters 8-37
Called from Wp__ProverWhy3.build_proof_task in file "src/plugins/wp/ProverWhy3.ml", line 1413, characters 8-59
There is an unexpected slash right the before .xml
file extension.