Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
---
layout: default
date: "30-11-2021"
short_title: Frama-C 24.0 (Chromium)
title: Release of Frama-C 24.0 (Chromium)
link: /fc-versions/chromium.html
---
Frama-C 24.0 (Chromium) is out. Download it [here](/fc-versions/chromium.html).
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