--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on April 2013 ---
Thank you for the new version! Trying to use WP to get a why3 output with the following program: /*@ axiomatic lists{ @ type list; @ logic list Nil; @ logic list Cons(integer i, list l); @ logic integer length ( list l); @ axiom nil_length: length(Nil)==0; @ axiom list_length: \forall list l; \forall integer i; @ length(Cons(i,l))== 1 + length(l);} */ /*@ ensures length(Cons(x,Nil))== 1;*/ void inst2(int x) { } The PO gets proven when using the Alt-ergo prover directly: Case 1: Alt-ergo $ frama-c -wp -wp-prover alt-ergo -wp-out toto2 example_wp.c [kernel] preprocessing with "gcc -C -E -I. example_wp.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Alt-Ergo] Goal typed_inst2_post : Valid (8ms) (3) However when using why3 the following error occurs: Case 2: Alt_ergo via why3 $ frama-c -wp -wp-prover why3:alt-ergo -wp-out toto2 example_wp.c [kernel] preprocessing with "gcc -C -E -I. example_wp.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled ------------------------------------------------------------ --- Why3 (stderr) : ------------------------------------------------------------ File "toto2/typed/A_lists.why", line 12, characters 5-11: syntax error ------------------------------------------------------------ [wp] [Alt-ergo] Goal typed_inst2_post : Failed Error: Why3 exits with status [1] Thank you, Romain Jobredeaux ----- Original Message ----- From: "Julien Signoles" <Julien.Signoles at cea.fr> To: "Frama-C public discussion" <frama-c-discuss at lists.gforge.inria.fr> Sent: Friday, April 19, 2013 11:02:11 AM Subject: [Frama-c-discuss] New Frama-C version: Fluorine Dear Frama-C users, We are glad to announce a new major release of Frama-C, named Fluorine-20130401. ======== DOWNLOAD ======== You can download the release at http://frama-c.com/download.html . For now, that is a source tar-ball distribution. A OPAM package is going to be available in the next few days. ============ MAIN CHANGES ============ This new major version includes too many bug fixes and improvements to list here: details are available at http://frama-c.com/Changelog.html. The main highlights are: - WP supports a new 'Typed' memory model - WP gets a Why3 output - RTE and Value are now consistent on annotations they emit - Value improves precision and support of ACSL annotations - (developers only) The kernel provides a new API for AST pretty printing For plug-in developers: this major release changes several Frama-C APIs in an incompatible way. Some of the plugin-side changes can automatically be applied by using the script bin/oxygen2fluorine.sh of the source distribution. Complex plug-ins should be reviewed for compatibility. ====== ENJOY! ====== Enjoy this release and please report any issue and/or successes with this version through the usual channels, listed at http://frama-c.com/support.html . For the Frama-C Development Team, Julien Signoles -- Researcher-engineer CEA LIST, Software Safety Labs tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr _______________________________________________ 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