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>
- Follow-Ups:
- [Frama-c-discuss] Frama-C 21 (Scandium) has been released!
- From: tjoppen at acc.umu.se (Tomas Härdin)
- [Frama-c-discuss] Frama-C 21 (Scandium) has been released!
- Prev by Date: [Frama-c-discuss] Eva plugin - asin function
- Next by Date: [Frama-c-discuss] Frama-C on a code subset?
- Previous by thread: [Frama-c-discuss] Frama-C fails to build on Debian
- Next by thread: [Frama-c-discuss] Frama-C 21 (Scandium) has been released!
- Index(es):