framac-24.0-beta.md

layout: default
date: "04-11-2021"
short_title: Frama-C 24.0-beta (Chromium)
title: Beta release of Frama-C 24.0-beta (Chromium)
link: /fc-versions/chromium.html

Frama-C 24.0-beta (Chromium) is out. Download it here.

Main changes with respect to Frama-C 23 (Vanadium) include:

Kernel

• support C11's _Static_assert
• support for flexible array members in nested struct (gcc machdeps only)
• fixes unsound reuse of recursive functions

E-ACSL

• new options for more precise reporting in case of failed assertion
• support for \sum, \prod and \numof

Eva

• new experimental taint domain for taint analysis
• new experimental multidim domain to improve analysis precision on arrays of structures and multidimensional arrays.
• new options for interprocedural states partitioning
• new dynamic_split annotation
• fixes soundness bugs in octagon and bitwise domains
• improve precision for octagon and symbolic-locations domains

Variadic

• translation of printf/scanf calls with non-constant formatting string (assuming arguments match the format)
• falls back to a generic translation if specialized one fails, to guarantee the absence of variadic calls after the plugin has run

WP

• removed -wp-overflows option, which was unsound
• experimental support for terminates clauses