--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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