Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c - wp on Windows/Cygwin

Thanks, Pascal,

Given your comments, I would expect that

 > frama-c -wp swap.c
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_swap_post_2 : Valid
[wp] [Alt-Ergo] Goal typed_swap_post : Failed
      Error: No such file or directory (alt-ergo)

is closest to working, but can't find alt-ergo, even though it is on the 
PATH.
Can you - or someone - comment on where wp expects alt-ergo (and under 
what name)  on Windows?

- David

On 11/2/2013 12:03 PM, Pascal Cuoq wrote:
> Hello,
>
> On Mon, Oct 28, 2013 at 6:13 PM, David Cok <dcok at grammatech.com 
> <mailto:dcok at grammatech.com>> wrote:
>
>     I would appreciate advice on what appears to be frama-c -wp
>     installation configuration issues on Windows 7/Cygwin.
>
>     I have Frama-C and Alt-Ergo installed and working independently.
>     However, toy programs give errors that are not explained in the
>     installation material:
>     [alt-ergo is on the PATH; swap.c is the example from the
>     installation manual, but the problems below occur for other
>     examples as well]
>
>     > frama-c -wp swap.c
>     [wp] Running WP plugin...
>     [wp] Collecting axiomatic usage
>     [wp] warning: Missing RTE guards
>     [wp] 2 goals scheduled
>     [wp] [Qed] Goal typed_swap_post_2 : Valid
>     [wp] [Alt-Ergo] Goal typed_swap_post : Failed
>          Error: No such file or directory (alt-ergo)
>
>     Why this error?
>
>     > frama-c -wp -wp-prover alt-ergo swap.c
>     ... same result as above
>
>     > frama-c -wp -wp-prover `which alt-ergo` swap.c
>     [kernel] preprocessing with "gcc -C -E -I.  swap.c"
>     [wp] Running WP plugin...
>     [wp] Collecting axiomatic usage
>     [wp] warning: Missing RTE guards
>     [wp] 2 goals scheduled
>     [wp] [Qed] Goal typed_swap_post_2 : Valid
>     [wp] [/cygdrive/c/cygwin/home/dcok/mybin/alt-ergo] Goal
>     typed_swap_post : Failed
>          Error: No such file or directory (why3)
>
>     Better except that
>     - alt-ergo is supposed to be able to solve this problem easily
>     - is the -wp-prover option expecting a *path*? If so, how do I
>     tell (an env. var.) what default path to use for alt-ergo?
>     - I don't have why3 installed - from the documentation it should
>     not be required - is there a way to tell frama-c not to try it?
>
>
> I am not an expert of WP, but perhaps my answer will get things rolling.
>
> Your second attempt,  "frama-c -wp -wp-prover alt-ergo swap.c" is 
> closest to something that should work, and I am surprised it doesn't. 
> The option -wp-prover does not expect a path to an executable, it 
> expects the name of a prover, specific built-in theories of which are 
> then used in the output destined to the prover. In the case of 
> Alt-Ergo, this would be any or all of the theories listed on 
> http://alt-ergo.lri.fr .
>
> The error message about why3 in your third attempts, "frama-c -wp 
> -wp-prover `which alt-ergo` swap.c" is probably due to the fact that 
> the WP plug-in did not recognize the name of a prover it knows as 
> argument to option -wp-prover, and somehow defaulted to why3.
>
> Pascal
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131103/a09bd66a/attachment.html>