--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2013 ---
[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>