[Frama-c-discuss] Frama-C Release Neon-20140301

François Bobot 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
http://frama-c.com/support.html .

For the Frama-C Development Team,
François Bobot
CEA LIST, Software Safety Labs

More information about the Frama-c-discuss mailing list