--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on March 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Sodium release



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