--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2020 ---
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>