Frama-C release 25.0 (Manganese)
Sources
Manuals
- acsl-1.18
- acsl-implementation
- aorai-example-25.0-Manganese.tgz
- aorai-manual
- e-acsl-1.18
- e-acsl-implementation
- e-acsl-manual
- eva-manual
- metrics-manual
- plugin-development-guide
- rte-manual
- user-manual
- wp-manual
Main changes
Kernel
- The experimental AST Diff module allows to compute difference between the AST of two projects
- significant changes in AST types that might break existing development
E-ACSL
- add support for Linux's pthread concurrency
EVA
- New public API to run the analysis and access its results, intended to replace the old API in Db.Value.
- Improved multidim domain: it is now more precise and more robust, and is able to infer simple array invariants and disjunctive struct invariants.
WP
- uses Why3 1.5.0
- new supported ACSL features : decreases clause and general measures for variant and decreases
- new tactics: Clear for hypothesis removal and ModMask for rewriting of mask and modulos
- removed deprecated legacy WP engine and native prover output (always use Why3)
- fixes loop invariant order and collect more hypotheses when proving them
Ivette (New Frama-C GUI)
We are introducing Ivette, a new GUI for Frama-C. In this preliminary version, only EVA and some of its derived plug-ins are supported.
Build & install instructions are in ivette/INSTALL.md
from the source tarball.
To try it, simply use ivette
in replacement of frama-c-gui
.
Your feedback is welcome.
Have fun !