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