Main changes with respect to Frama-C 22 (Titanium) include:
Kernel
- New
admit
annotations (which already acceptedassert
andcheck
) to express hypotheses to be admitted but not verified by Frama-C - Set default machdep to
x86_64
; allow setting machdep via environment variableFRAMAC_MACHDEP
AORAI
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva
E-ACSL
- Add runtime support for Windows
- Add support for loop variant
- Add support for multiple binders in guarded quantifications
EVA
- Partial support for recursion: new option
-eva-unroll-recursive-calls
to precisely analyze the n first recursive calls, before using the function specification to interpret the remaining calls - Improved automatic widening thresholds
- Improved automatic loop unroll
WP
- New internal WP engine, fixing many issues related to control flow graph and local variable scoping. Support for stmt contracts has been removed. Support for looping gotos has been removed. Altough unsound, the legacy engine is still accessible via
-wp-legacy
option - Bump Why3 version to 1.4.0
- Section « Limitation & Roadmap » added to the WP manual