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