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

  • Subject: [Frama-c-discuss] Sodium release
  • From: francois.bobot at cea.fr (François Bobot)
  • Date: Tue, 17 Mar 2015 18:16:31 +0100
Dear Frama-C users,

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

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

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 soon[1].

============
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:
- [kernel] Frama-C standard library is included by default (-no-frama-c-stdlib
    for the previous behavior)

- [kernel] When preprocessor supports it, expansions of macros in
   annotations (-pp-annot) is now done by default. Efficiency of
   -pp-annot has been greatly improved.

- [kernel] the default machdep no longer assumes the compiler is gcc. See
    'frama-c -machdep help'

- [*] Homogenization of collections options (eg: -cpp-extra-args, -slevel-function)

- [value] much-improved pretty-printing of pointer abstract values

- [value] logic ranges are now evaluated using a dedicated domain,
    resulting in faster analysis and more precise results

- [value] the parameters of a function call may be reduced if they are
    constrained by the callee

- [kernel, value] support for \dangling predicate

- [kernel, value, WP] support for const variables

- [rte, value] alarms are now emitted for casts from floating-point to integer
    that overflow

- [from] assigns/from acsl clauses of functions with a body can now be verified
    through option -from-verify-assigns

- [from] major performance improvements on large input programs.

- [semantic constant folding] better propagation on pointer variables

For plug-in developers:
- New API for collections options
- New AST nodes Throw and TryCatch for dealing with exception. The C
   front-end does not generate any such node. A code transformation can
   compile such nodes away if needed (see src/kernel/exn_flow.mli for
   more information).

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

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 .

[1] https://github.com/ocaml/opam-repository/pull/3755

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