|
|
|
# Frama-C release 24.0 (Chromium)
|
|
|
|
## Sources
|
|
|
|
- [frama-c-24.0-Chromium.tar.gz](downloads/frama-c-24.0-Chromium.tar.gz)
|
|
|
|
|
|
|
|
## Manuals
|
|
|
|
- [acsl-1.17](manuals/acsl-1.17.pdf)
|
|
|
|
- [acsl-implementation](manuals/acsl-implementation-24.0-Chromium.pdf)
|
|
|
|
- [aorai-example-24.0-Chromium.tgz](manuals/aorai-example-24.0-Chromium.tgz)
|
|
|
|
- [aorai-manual](manuals/aorai-manual-24.0-Chromium.pdf)
|
|
|
|
- [e-acsl-1.17](manuals/e-acsl-1.17.pdf)
|
|
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation-24.0-Chromium.pdf)
|
|
|
|
- [e-acsl-manual](manuals/e-acsl-manual-24.0-Chromium.pdf)
|
|
|
|
- [eva-manual](manuals/eva-manual-24.0-Chromium.pdf)
|
|
|
|
- [metrics-manual](manuals/metrics-manual-24.0-Chromium.pdf)
|
|
|
|
- [plugin-development-guide](manuals/plugin-development-guide-24.0-Chromium.pdf)
|
|
|
|
- [rte-manual](manuals/rte-manual-24.0-Chromium.pdf)
|
|
|
|
- [user-manual](manuals/user-manual-24.0-Chromium.pdf)
|
|
|
|
- [wp-manual](manuals/wp-manual-24.0-Chromium.pdf)
|
|
|
|
|
|
|
|
## Main changes
|
|
|
|
### 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 |
