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>
- Prev by Date: [Frama-c-discuss] Assigns-clauses in preconditions and ghost variable assignment
- Next by Date: [Frama-c-discuss] PhD defense Guillaume Davy - 12/6/2018 - Generation of codes and provable annotations of interior-point algorithms for critical embedded systems
- Previous by thread: [Frama-c-discuss] Assigns-clauses in preconditions and ghost variable assignment
- Next by thread: [Frama-c-discuss] PhD defense Guillaume Davy - 12/6/2018 - Generation of codes and provable annotations of interior-point algorithms for critical embedded systems