[Frama-c-discuss] Frama-C Release Neon-20140301
francois.bobot at cea.fr
Wed Mar 12 18:21:27 CET 2014
Dear Frama-C users,
We are glad to announce a new major release of Frama-C, named
You can download the release at http://frama-c.com/download.html .
For now, that is a source tar-ball distribution. An OPAM package will be
available in the next few days.
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:
- The Value plugin is more efficient (computation and cache have been
optimized). The experimental option -val-show-perf helps estimating
which part of the C code takes time to analyze. One can send SIGUSR1
signal to a Frama-C process for stopping and saving the
partial results of the Value plugin.
- The From plugin computes separately data dependencies and indirect
(address, control) dependencies with option -show-indirect-deps
- The axiomatizations used by the WP plugin are now shared between the
different prover outputs and mainly realized in Coq thanks to a better
integration with Why3.
For plug-in developers:
- The api for Dataflow have been greatly simplified.
- This major release changes several Frama-C APIs
in an incompatible way. Some of the plugin-side changes can
be automatically applied by using the script bin/fluorine2neon.sh of
the source distribution. Complex plug-ins should be reviewed for
Enjoy this release and please report any issue and/or
successes with this version through the usual channels, listed at
For the Frama-C Development Team,
CEA LIST, Software Safety Labs
More information about the Frama-c-discuss