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] Release of the Silicon version of Frama-C

  • Subject: [Frama-c-discuss] Release of the Silicon version of Frama-C
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Mon, 5 Dec 2016 18:23:49 +0100
Dear all,

We are delighted to announce the release of the Silicon [1] version of
Frama-C, available at [2].  You will find below a summary of the more
important changes. An exhaustive list can be found in the Changelog. We
would like to thank all of you for the feedback we received on the release
candidate version, on this list or privately. This led to a number of bug
fixes, detailed at the beginning of the Changelog.

The documentation for the kernel and the plugins has been updated, and can
be found on the download page. The Opam package will be available soon.
Reports about possible regressions (or improvements!) on your favorite code
or plugin remain very welcome.


Main changes:

# Kernel:
- refactoring of ACSL extensions + allow extensions in loop annotations
- rename multiple types of the logic AST for more coherence

# Libc:
- The implementations of some functions of the standard library are now
available in share/libc/*.c. The .c and .h files in share/libc are
deprecated.

# Eva/Value plugin:
- two now (experimental) analysis domains are available. Gauges infer
affine relations between variables in loops. Symbolic locations keep track
of the contents of l-values such as *p or t[i].
- new builtins are available for dynamic allocation, and some functions of
string.h and. Default builtins can be activated through option
-val-builtins-auto.

# WP plugin:
- unified variable usage for all models
- WP now honors the kernel option -warn-(signed|unsigned)-(overflow|downcast).
The cint and cfloat are used by default

# Rte plugin:
- new option -rte-pointer-call, to generate annotations for calls through
function pointers.

# Nonterm plugin:
- overall increase in precision, especially on compound statements (if,
switch, loops...).

# Changes in the compilation process:
- OCamlGraph is no longer packaged within Frama-C, and must be installed to
build Frama-C from source.
- OCaml version greater or equal than 4.02.3 required.

Happy verification using Frama-C!

<https://github.com/Frama-C/Frama-C-snapshot/tree/Silicium-rc1>
[1] Thanks to Jens for tactfully reminding us that Silicium is a frenchism!
[2] http://frama-c.com/download.html
<https://github.com/Frama-C/Frama-C-snapshot/tree/Silicium-rc1>
<https://github.com/Frama-C/Frama-C-snapshot/tree/Silicium-rc1>

-- 
Boris, for the Frama-C development team.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161205/33f781e2/attachment.html>