Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] [wp] invoke provers from command line
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Mon, 9 Dec 2013 00:22:00 -0500
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>