Frama-C 21.0 (Scandium) release.
Main changes with respect to Frama-C 20 (Calcium) include:
Kernel
- new option
-warn-invalid-pointer
(disabled by default; warns on pointer arithmetic resulting in invalid values) - new option
-warn-pointer-downcast
(enabled by default; warns when a pointer/integer conversion may lead to loss of precision) - improved ghost support: ghost else, and check that ghost code does not alter normal control flow
- constfold can now use value of const globals
Eva
- New option
-eva-domains
to enable a list of analysis domains (replacing the former options-eva-name-domain
).-eva-domains help
prints the list of available domains with a short description - New option
-eva-domains-function
to enable domains only on given functions - When
-warn-invalid-pointers
is enabled, emits alarms on invalid pointer arithmetics resulting in a pointer that does not point inside an object or one past an object (even if the pointer is not used afterward) - The subdivision of evaluations can now be enabled locally:
- on given functions through option
-eva-subdivide-non-linear-function
- on specific statements via
/*@ subdivide N; */
annotations.
- on given functions through option
WP
- Upgraded Why3 backend (requires why3 1.3.1)
- Support for IEEE float model (why3 provers only)
- Smoke Tests : attempt to find inconsistencies or dead code from requirements (see
-wp-smoke-tests
option in WP manual) - Many improvements in lemmas, tactics and cache management (see full WP Changelog for details).
E-ACSL
- Better support of complex jumps for goto and switch statements