--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Release candidate of Frama-C Silicium



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>