--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on November 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Beta release of Frama-C 20.0 (Calcium)



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>