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) has been released!

  • Subject: [Frama-c-discuss] Frama-C 18 (Argon) has been released!
  • From: david.buhler at cea.fr (David Bühler)
  • Date: Thu, 29 Nov 2018 16:41:53 +0100
Dear list,

It is with utmost pleasure that we announce the release of Frama-C 18.0 
(Argon),
on the same date that the tomb of the pharaoh Tutankhamun was opened in the
Valley of the Kings, 96 years ago. We hope, however, to avoid any curse.

Main changes with respect to Frama-C 17 (Chlorine) 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 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])/


The Frama-C github repository has been updated: 
https://github.com/Frama-C/Frama-C-snapshot
New opam packages will be available soon.
A complete changelog can be found at: http://frama-c.com/changelog.html
Sources and manuals are available at: http://frama-c.com/download.html

Please don't hesitate to try it out and to provide feedback; reports about
possible regressions or improvements on your favorite code are very welcome.

Happy verification with Frama-C!

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