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

[Frama-c-discuss] [wp] invoke provers from command line



Hi all,
   I just started with the wp plugin. 
   I was trying out the -wp-prover options, as listed in its help manual:

-wp-prover <dp,...>  Submit proof obligations to external prover(s):
                    - 'none' to skip provers
                    Directly supported provers:
                    - 'alt-ergo' (default)
                    - 'altgr-ergo' (gui)
                    - 'coq', 'coqide' (see also -wp-script)
                    - 'why3:<dp>' or '<dp>' (why3 prover, see -wp-detect)
                    - 'why3ide' (why3 gui)


I'd like to try the last two options. the demo file, max.c,  is attached.
When I use why3ide option, I got the following output:
-----------------------------------------------------------------------------
$ frama-c -wp -pp-annot -wp-prover why3ide max.c
[kernel] preprocessing with "gcc -C -E -I.  -dD src/max.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] Goal typed_max_post : trivial
[wp] Goal typed_max_post_2 : trivial
[wp] Goal typed_max_assert : trivial
------------------------------------------------------------------------------
why3IDE did not show up. It seems that all VCs are proved already, right? is there a way to display the why3IDE interface using wp?
   
   Thanks!

cheers
xiao-lei
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131209/d4b145cb/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: max.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131209/d4b145cb/attachment-0001.c>