--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C 21 (Scandium) has been released!



Dear list,

It is with utmost pleasure that we celebrate the 155 years of the Battle 
of the Riachuelo by announcing the release of *Frama-C 21.0 (Scandium)*.

A complete changelog can be found at: http://frama-c.com/changelog.html
Sources and manuals are available at: http://frama-c.com/download.html

The new opam package is already available : run `opam update && opam 
install frama-c.21.0` to upgrade.

The release is also available in our public Gitlab repository: 
https://git.frama-c.com/pub/frama-c/-/releases

(As a reminder, the Github snapshot repository is no longer being updated.)

Note that this is the last Frama-C release compatible with OCaml < 
4.08.1; Frama-C 22 (Titanium) will require OCaml >= 4.08.1.


Main changes with respect to Frama-C 20 (Calcium) include:


*Kernel*

- new option -warn-invalid-pointer (disabled by default; warns on 
pointer arithmetic resulting in invalid values)

- new option -warn-pointer-downcast (enabled by default; warns when a 
pointer/integer conversion may lead to loss of precision)

- improved ghost support: ghost else, and check that ghost code does not 
alter normal control flow

- constfold can now use value of const globals


*Eva*

- New option -eva-domains to enable a list of analysis domains 
(replacing the former options -eva-name-domain). "-eva-domains help" 
prints the list of available domains with a short description

- New option -eva-domains-function to enable domains only on given functions

- When -warn-invalid-pointers is enabled, emits alarms on invalid 
pointer arithmetics resulting in a pointer that does not point inside an 
object or one past an object (even if the pointer is not used afterward)

- The subdivision of evaluations can now be enabled locally:

     - on given functions through option -eva-subdivide-non-linear-function

     - on specific statements via /*@ subdivide N; */ annotations.



*WP*

- Upgraded Why3 backend (requires why3 1.3.1)

- Support for IEEE float model (why3 provers only)

- Smoke Tests : attempt to find inconsistencies or dead code from 
requirements (see -wp-smoke-tests option in WP manual)

- Many improvements in lemmas, tactics and cache management (see full WP 
Changelog for details).


*E-ACSL*

- Better support of complex jumps for |goto| and |switch| statements


And a *new plug-in, Instantiate*, to generate function specializations 
e.g. for functions with void* (memcpy/memset/etc), to help other plugins 
such as WP.


Happy analysis with Frama-C!


For the Frama-C team,
--
André Maroneze
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200612/db699fa0/attachment.html>