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] Beta release of Frama-C 21.0 (Scandium)

  • Subject: [Frama-c-discuss] Beta release of Frama-C 21.0 (Scandium)
  • From: Andre.MARONEZE at cea.fr (Andre Maroneze)
  • Date: Mon, 18 May 2020 08:50:52 +0200
Dear Frama-C enthusiasts,


We have the pleasure to announce the beta release of Frama-C 21 (Scandium).

It is available in the stable/scandium branch of Frama-C's public git 
repository: https://git.frama-c.com/pub/frama-c/-/tree/stable/scandium, 
tagged 21.0-beta.

A link to a tar.gz archive and the manuals are available at 
https://git.frama-c.com/pub/frama-c/-/wikis/Frama-C-21.0-beta-Scandium

You are encouraged to try it out and report any potential regressions on 
this list or on https://git.frama-c.com/pub/frama-c/-/issues

Barring any critical issues, the final Frama-C 21 release is scheduled 
for June.

*
*

*Main changes 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!

André, for the Frama-C team

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200518/633ecc94/attachment.html>