--- layout: fc_discuss_archives title: Message 6 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



Hello,

On Mon, Oct 28, 2013 at 6:13 PM, David Cok <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131102/bba2120c/attachment.html>