--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on October 2013 ---
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