--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on November 2019 ---
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>