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>