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 cea.fr (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
included.

========
DOWNLOAD
========

You can download the release at http://frama-c.com/download.html .
For now, that is a source tarball distribution. An OPAM package will be
available soon.

============
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:
  - [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, 
\is_minus_infinity)
  - [report] new report in .csv format


======
ENJOY!
======

Enjoy this release and please report any issues with this version
through the usual channels, listed at http://frama-c.com/support.html .
Positive feedback is also welcome.

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