--- layout: fc_discuss_archives title: Message 6 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



Hi again,

Two additional information:

- you can download the release from this Github page:
https://github.com/Frama-C/Frama-C-snapshot/releases
- we plan to release the final version of Silicium in 3-4 weeks, depending
on the feedback we get

Cheers,

On Fri, Oct 28, 2016 at 2:24 PM, Boris Yakobowski <boris at yakobowski.org>
wrote:

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



-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161028/60fc84e6/attachment.html>