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: dcok at grammatech.com (David Cok)
  • Date: Mon, 28 Oct 2013 13:13:38 -0400
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?

Thanks,

David