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

[Frama-c-discuss] New Frama-C version: Fluorine



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