On Thu, Jun 18, 2020 at 5:31 AM Richard W.M. Jones <rjones(a)redhat.com> wrote:
I was trying to run through the tutorial here:
https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
The first example on page 15 & 16 fails with:
[wp] Running WP plugin...
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
I couldn't get any further. What I tried was:
- Install both why3 and alt-ergo. Why aren't they deps of frama-c?
Historically, they were not required for frama-c to do something
useful. The WP plugin needs them, but frama-c can be used in other
ways.
However, I see that frama-c's opam file lists both of them as
non-optional "depends", so I will make them Requires for the next
frama-c build. (Note that alt-ergo is a Suggests already.)
- Run /usr/lib64/why3/commands/why3config by hand (why isn't it
in
/usr/bin?), which creates $HOME/.why3.conf
I see you figured this one out already.
- stracing the program, it seems like it never attempts to
open or run anything to do with alt.*ergo
I see this in the log:
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
which is a lie. Prover alt-ergo is most definitely listed in
why3.conf. I'll debug this. Stand by.
--
Jerry James
http://www.jamezone.org/