--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on October 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C 18 (Argon) - beta



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>