--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2013 ---
Thanks, Pascal, Given your comments, I would expect that > 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) is closest to working, but can't find alt-ergo, even though it is on the PATH. Can you - or someone - comment on where wp expects alt-ergo (and under what name) on Windows? - David On 11/2/2013 12:03 PM, Pascal Cuoq wrote: > Hello, > > On Mon, Oct 28, 2013 at 6:13 PM, David Cok <dcok at grammatech.com > <mailto: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 > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131103/a09bd66a/attachment.html>