--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on December 2019 ---
Dear list, It is with utmost pleasure that we celebrate the 153th birthday of Vassily Kandinsky by announcing the release of *Frama-C 20.0 (Calcium)*. We take this opportunity to also announce the *opening of the development branch of Frama-C*, powered by Gitlab: https://git.frama-c.com/pub/frama-c Unlike the Github snapshot repository (updated at each release), this is a mirror of the master branch of our internal Git repository, updated daily. We intend this repository to be the main entry point for issues and merge requests coming from the community, and hope that you will find it useful. Coming back to the release: As usual, a new opam package will be available soon. The Frama-C github repository has been updated: https://github.com/Frama-C/Frama-C-snapshot (it is being obsoleted; future releases will be directly available from our Gitlab repository) A complete changelog can be found at: http://frama-c.com/changelog.html Sources and manuals are available at: http://frama-c.com/download.html Main changes with respect to Frama-C 19 (Potassium) 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. Please don't hesitate to try it out and to provide feedback; reports about possible regressions or improvements on your favorite code are very welcome. Happy verification with Frama-C! For the Frama-C team, -- André Maroneze -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191204/e0d7643d/attachment.html>