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 20.0 (Calcium)
- Subject: [Frama-c-discuss] Beta release of Frama-C 20.0 (Calcium)
- From: Andre.MARONEZE at cea.fr (Andre Maroneze)
- Date: Wed, 6 Nov 2019 16:30:42 +0100
Dear Frama-C enthusiasts, We have the pleasure to announce the beta release of Frama-C 20 (Calcium). It is available in the latest branch of Frama-C-snapshot's repository on github: https://github.com/Frama-C/Frama-C-snapshot/tree/latest A link to a tar.gz archive and the manuals are available at https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-20.0-beta-Calcium You can also try it on opam using the following command: opam pin add frama-c "https://github.com/Frama-C/Frama-C-snapshot.git#latest" You are encouraged to try it out and report any potential regressions on this list, on https://bts.frama-c.com or on https://github.com/Frama-C/Frama-C-snapshot/issues. Barring any critical issues, the final Frama-C 20 release is scheduled for early December. *Main changes include:* *Kernel* - the minimum required OCaml version is now 4.05.0 - more strict checks related to ghost variables in non-ghost code, and support for ghost parameters - visitor behavior functions were moved from Cil to a new module Visitor_behavior *Eva* - New octagon domain inferring relations of the form Â a â¤ Â±XÂ±Y â¤ b between pairs of integer variables X and Y. - New option "-eva-auto-loop-unroll N", to unroll all Â loops whose number of iterations can be easily bounded by <N>. - Dynamic registration of abstract values and domains: Â developers of new domains no longer need to modify Eva's engine. *WP* - Use native Why3 API (now requires why3 at compile time); deprecated native alt-ergo & coq output - New cache mechanism for why3 provers, see -wp-cache option *E-ACSL* - Support of rational numbers and operations. And a *new plug-in, Markdown-report* (MdR), to generate reports in both Markdown and SARIF formats. AndrÃ©, for the Frama-C team -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191106/79b901ab/attachment.html>