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 19:29:15 +0200
  • In-reply-to: <CABbVA-DVgjLP=t3MQeZSHAgaP4OZ-S2rktXCyZGJ-KJVVi+6Mw@mail.gmail.com>
  • References: <CABbVA-DVgjLP=t3MQeZSHAgaP4OZ-S2rktXCyZGJ-KJVVi+6Mw@mail.gmail.com>
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>