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] Frama-C 21 (Scandium) has been released!

  • Subject: [Frama-c-discuss] Frama-C 21 (Scandium) has been released!
  • From: Andre.MARONEZE at cea.fr (Andre Maroneze)
  • Date: Fri, 12 Jun 2020 08:49:38 +0200
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>