On Thu, Jun 18, 2020 at 03:15:13PM -0600, Jerry James wrote:
> On Thu, Jun 18, 2020 at 9:01 AM Jerry James wrote:
> > 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
On Thu, Jun 18, 2020 at 9:01 AM Jerry James wrote:
> 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.
Run "why3 config --full-config", then start frama-c
On Thu, Jun 18, 2020 at 5:31 AM Richard W.M. Jones 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
On Thu, Jun 18, 2020 at 12:31:44PM +0100, Richard W.M. Jones wrote:
> - Run /usr/lib64/why3/commands/why3config by hand (why isn't it in
>/usr/bin?), which creates $HOME/.why3.conf
So the reason it's not in /usr/bin is because you have to run it like
this:
$ why3 config --detect
Found prover
On 2020-06-18 19:31, Richard W.M. Jones 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 wh
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:
-
