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