--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on June 2016 ---
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