[WP] Isabelle/HOL driver does not work
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 test.h
- Observe the following output:
[wp] 1 goal scheduled
[wp] [Unknown] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Unknown: 1
- Observe that no new files or directories are created.
Expected behavior
Some generated files/directories that can be used to prove the goal in Isabelle/HOL.
Actual behavior
Nothing is generated, and no errors are reported. The verification fails silently without any clue about what went wrong.
Contextual information
- Frama-C: 26.0 (Iron) installed with
opam
- Why3: 1.5.1 installed with
opam
- Isabelle: 2021-1
- OS: Ubuntu 22.04.1 LTS