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_1e1724d1-f6ef-6a8b-a2ba-3f58139228dd@cea.fr>
  • References: <30209_1589784643_5EC23042_30209_11852_1_1e1724d1-f6ef-6a8b-a2ba-3f58139228dd@cea.fr>
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>