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

  • Subject: [Frama-c-discuss] Aluminium release
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Wed, 1 Jun 2016 16:09:05 +0200
Dear Frama-C users,

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

========
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 major version fixes many bugs and includes improvements
(details are available at http://frama-c.com/Changelog.html)
and three new plug-ins.

The main highlights are:
- [variadic] new plug-in which translates variadic functions, calls and
   macros to allow analyses to handle them more easily.
- [loop] new plug-in which estimates loop bounds and -slevel-function
   parameters.
- [nonterm] new plug-in for detection of definite non-termination based on
   Value.
- [value] major reimplementation of large parts of the plugin. New analysis
   domains are available (see options -eva-equality-domain and
   -eva-bitwise-domain), and the analysis of conditionals has been
   improved. 'direct' and 'indirect' annotations are now used to evaluate
   assigns clauses. Better propagation strategy for nested loops and changes
   in the widening strategy for frontiers of integer types.
- [cil] various improvements to the handling of empty structs, zero-length
   arrays, and flexible array members.
- [kernel] automatic generation of assigns from GCC's extended asm.
- [ACSL] new predicate \valid_function, requiring the compatibility
   between the type of the pointer and the function being pointed (currently
   supported by Value), notation { x, y, z } for defining sets and built-in
   operators for lists (currently supported by WP).

======
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.

The major releases of Frama-C are now available on Github at
https://github.com/Frama-C/Frama-C-snapshot.
Pull requests are welcome!

-- The Frama-C Development Team