Main changes with respect to Frama-C 21 (Scandium) include:


  • OCaml version greater than or equal to 4.08.1 required.
  • introduce check-only annotations for requires, ensures, loop invariant and lemmas
  • \from now accepts &v expressions
  • add option -print-config-json, to output Frama-C configuration data in JSON format
  • new option -explain, which provides help messages for options used on the command line
  • add option -print-cpp-commands, to print the preprocessing commands used by Frama-C
  • support for C11's _Noreturn and _Thread_local specifiers
  • allows for axiomatic blocks-like extensions


  • Ya automata can set auxiliary variables during a transition, and use such variables in subsequent guards.


  • support of bitwise operators
  • support of \separated
  • support of complete and disjoint behaviors
  • support of logical array comparisons


  • easier setup of dynamic allocation builtins: new option -eva-alloc-builtin to configure uniformly their behavior (instead of mapping each malloc/calloc/realloc function to the corresponding builtin), and new annotation eva_allocate to locally override the global option
  • new builtins for trigonometric functions acos, asin and atan (and their single-precision version acosf, asinf, atanf)
  • improved automatic loop unroll (-eva-auto-loop-unroll option) on loops with several exit conditions, conditions using equality operators, temporary variables introduced by the Frama-C normalization or goto statements

Markdown Report

  • update Sarif output to 2.1.0 and prettier URI


  • the generated code is now compilable and compatible with E-ACSL


  • upgraded Why3 backend (requires why3 1.3.3)
  • support of the \initialized ACSL predicate
  • support for generalized check-only ACSL annotations
  • added support for Why3 interactive prover (Coq)
  • new tactic Bit-Test range
  • memory model hypotheses warnings are more precise
  • new experimental option: -wp-check-memory-model to automatically check memory model hypotheses
  • new warning pedantic-assigns. WP needs precise assigns ... \from ... specification about out pointers to generate precise proof hypotheses