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.

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