--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2016 ---
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>