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] Frama-C 18 (Argon) - beta

  • Subject: [Frama-c-discuss] Frama-C 18 (Argon) - beta
  • From: david.buhler at cea.fr (David Bühler)
  • Date: Wed, 31 Oct 2018 16:43:19 +0100
Dear Frama-C enthusiasts,

We have the pleasure to announce the beta release of Frama-C 18 (Argon).

It is available in the latest branch of Frama-C-snapshot's repository on 
github: https://github.com/Frama-C/Frama-C-snapshot/tree/latest
A link to a tar.gz archive and the manuals are available at 
https://github.com/Frama-C/Frama-C-snapshot/wiki/Frama-C-18.0-beta-Argon
You can also try it on opam using the following command: /opam pin add 
frama-c "https://github.com/Frama-C/Frama-C-snapshot.git#latest"/

You are encouraged to try it out and report any potential regression on 
this list,
on https://bts.frama-c.com or on 
https://github.com/Frama-C/Frama-C-snapshot/issues.

Barring any critical issue, the final Frama-C 18 release is scheduled 
for late November.

Main changes include:

### Kernel:
- Improved command-line options for treatment of warning categories:
   -plugin-warn-key category=status will set the status of category,
   instead of using 7 options -plugin-warn-abort, -plugin-warn-feedback, …
   with awkward ± categories
- All errors emitted during a run will now lead to a non-zero exit status
   of frama-c command line
- options for emitting an alarm on [left|right] shift of a negative
   value are now at kernel level (and removed from Eva)
- const globals are now unconditionally constants (option -const-writable is
   removed)
- several improvements to the frama-c libc specifications
- new binary frama-c-script to help with case studies

### Eva:
- Eva is now consistently named "Eva", and all its options start with -eva
   (compatibility with previous option names has been preserved).
- New "//@ loop unroll N;" annotations to unroll exactly the N first 
iterations
   of a loop, as an improvement over slevel options.
- The memexec cache is compatible with all domains, and is enabled by 
default.
   This cache greatly improves the analysis time.
- Builtins for memset and memcpy are now included in the open-source 
release.
- Alternative domains use the frama-c libc specification when a builtin 
is used,
   to minimize the loss of precision.
- Emits alarms when reading potential trap representations of type _Bool.
- New experimental domain numerors inferring absolute and relative errors of
   floating-point computations. Does not handle loops for now.

### E-ACSL:
- support of ranges in memory built-ins, e.g. /\valid(t+(0..9))/
- support of \at on logic variables, e.g. /\forall integer i; 0 <= i < 
10 ==> t[i] == \old(t[i])/


For the Frama-C team,
  --
David.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181031/79f507e5/attachment.html>