25.0-Manganese release

_events/framac-25.0.md

+---
+layout: default
+date: "21-06-2022"
+short_title: Frama-C 25.0 (Manganese)
+title: Release of Frama-C 25.0 (Manganese)
+link: /fc-versions/manganese.html
+---
+
+Frama-C 25.0 (Manganese) is out. Download it [here](/fc-versions/manganese.html).
+
+Main changes with respect to Frama-C 24 (Chromium) include:
+
+#### 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 !