--- layout: default date: 12-06-2020 short_title: Frama-C 21.0 (Scandium) title: Release of Frama-C 21.0 (Scandium) link: /fc-versions/sandium.html --- Frama-C 21.0 (Scandium) is out. Download it [here](/fc-versions/scandium.html). 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. #### 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 And a new plug-in, Instantiate, to generate function specializations e.g. for functions with `void*` (`memcpy`/`memset`/etc), to help other plugins such as WP. A complete changelog can be found [here](/html/changelog.html#Scandium-21.0).