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] Frama-C Release Neon-20140301

  • Subject: [Frama-c-discuss] Frama-C Release Neon-20140301
  • From: francois.bobot at (François Bobot)
  • Date: Wed, 12 Mar 2014 18:21:27 +0100

Dear Frama-C users,

We are glad to announce a new major release of Frama-C, named


You can download the release at .
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

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/ 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,
Fran?ois Bobot
CEA LIST, Software Safety Labs