framac-18.0.md

layout: default
date: 29-10-2018
event: Frama-C 18.0 (Argon)
title: Release of Frama-C 18.0 (Argon)

Frama-C 18.0 (Argon) is out. Download it here.

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])

A complete Changelog can be found here.