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

  • Subject: [Frama-c-discuss] Frama-c - wp on Windows/Cygwin
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sat, 2 Nov 2013 17:03:46 +0100
  • In-reply-to: <526E9B42.6060708@grammatech.com>
  • References: <526E9B42.6060708@grammatech.com>
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>