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] Magnesium release

  • Subject: [Frama-c-discuss] Magnesium release
  • From: francois.bobot at (François Bobot)
  • Date: Mon, 18 Jan 2016 16:15:58 +0100

Dear Frama-C users,

We are glad to announce a new major release of Frama-C, named
Magnesium-20151002. Intellectual property problems delayed this release, we
are very sorry for that. In the future we will setup clear guidelines for
contributions, to ensure that developments from the community are correctly


You can download the release at .
For now, that is a source tarball distribution. An OPAM package will be
available soon.


This new major version includes too many bug fixes and improvements to
list here: details are available at .

The main highlights are:
  - [value] brand new GUI, found in the "Values" tab
  - [value] new builtins for floating-point functions of the standard library
  - [value] more fine-grained control on the value of padding after initialisation
  - [value] multiple improvements to option -subdivide-float-var
  - [wp] many improvements for user experience (see Changelog)
  - [wp] many new or improved simplifications in Qed (see Changelog)
  - [wp] support for global const (see -wp-init-const option)
  - [wp] refined memory access and compound encoding
  - [wp] new memory model 'Caveat' for unit-proofs
  - [wp] new (less precise) integer model 'rg' to simplify integral ranges
  - [wp] more ACSL builtins (\subset, \is_NaN, \is_finite, \is_infinite, \is_plus_infinity, 
  - [report] new report in .csv format


Enjoy this release and please report any issues with this version
through the usual channels, listed at .
Positive feedback is also welcome.

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