Release 26.0-Iron

On behalf of "David Bühler" david.buhler@cea.fr (@buhler)

_events/framac-26.0.md

+---
+layout: default
+date: "23-11-2022"
+short_title: Frama-C 26.0 (Iron)
+title: Release of Frama-C 26.0 (Iron)
+link: /fc-versions/iron.html
+---
+
+Frama-C 26.0 (Iron) is out. Download it [here](/fc-versions/iron.html).
+
+Main changes with respect to Frama-C 25.0 (Manganese) include:
+
+The Frama-C build now uses dune. Hopefully, this should have no impact on most
+Frama-C users.
+Maintainers of external plug-ins must now use dune as well (see the plug-in
+migration section in the developer manual), and the loading of modules and
+scripts has changed (see the frama-c-build-scripts.sh tool to build scripts
+for Frama-C).
+
+#### Kernel
+- `calls` ACSL extension for listing potential targets of indirect calls is now
+  supported within kernel, and not only by the WP plug-in.
+
+#### Aoraï
+- remove (almost unused) support for LTL and Promela as input language.
+- support for programs with indirect calls if they are annotated with `calls`
+  annotations.
+
+#### E-ACSL
+- add support for logic functions returning a rational number.
+
+#### Eva
+- complete the Eva public API; the Db.Value API is now deprecated.
+- allow reducing the value of arguments of functions interpreted by a builtin
+  or an ACSL specification; this is especially useful on C asserts.
+- improved precision and performance of the octagon domain.
+
+#### WP
+- improved Json output for verification statistics and results.
+- Why3 version bumped to 1.5.1.
+
+#### Ivette (new Frama-C GUI)
+- the installation of Frama-C provides an installation script for Ivette.
+  Run 'ivette' once to finalize installation (this requires node 16, yarn and
+  an internet connection).
+- improve the dataflow graphs generated by the Dive plug-in.
+- when the taint domain of Eva is enabled, taint status of lvalues is shown
+  in the Inspector component and in Dive graphs.