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] Frama-C 20 (Calcium) has been released!

  • Subject: [Frama-c-discuss] Frama-C 20 (Calcium) has been released!
  • From: Andre.MARONEZE at cea.fr (Andre Maroneze)
  • Date: Wed, 4 Dec 2019 18:00:00 +0100
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>