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 candidate of Frama-C Silicium

  • Subject: [Frama-c-discuss] Release candidate of Frama-C Silicium
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Fri, 28 Oct 2016 14:24:24 +0200
Dear all,

It is great our pleasure to announce that a release candidate version for
Frama-C Silicium is now available on Github [1]. You will find below a
summary of the more important changes. Updated documentation is
forthcoming. Reports about possible regressions (or improvements!) on your
favorite code or plugin are very welcome.

# 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!

[1] https://github.com/Frama-C/Frama-C-snapshot/tree/Silicium-rc1

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