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: Tue, 19 May 2020 16:35:10 +0200
- In-reply-to: <30209_1589784643_5EC23042_30209_11852_1_1e1724d1firstname.lastname@example.org>
- References: <30209_1589784643_5EC23042_30209_11852_1_1e1724d1email@example.com>
It has been brought to our attention (https://git.frama-c.com/pub/frama-c/-/issues/12) that, due to the change of version of Why3 (previously 1.2.x, now 1.3.x), existing .why3.conf files may not work with the beta release. We thus recommend that, if you intend to use WP, please follow these instructions after installing Why3 1.3.1: rm ~/.why3.conf why3 config --full-config Best regards, On 18/05/2020 08:50, Andre Maroneze wrote: > > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- AndrÃ© Maroneze Researcher/Engineer CEA/List Software Reliability and Security Laboratory -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200519/09ed8fcf/attachment.html>
- Prev by Date: [Frama-c-discuss] Frama-C not parsing unicode.
- Next by Date: [Frama-c-discuss] Frama-c-discuss Digest, Vol 143, Issue 17
- Previous by thread: [Frama-c-discuss] Beta release of Frama-C 21.0 (Scandium)
- Next by thread: [Frama-c-discuss] Frama-c-discuss Digest, Vol 143, Issue 12