Main changes since 25.0 Manganese

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 tool to build scripts for Frama-C).


  • calls ACSL extension for listing potential targets of indirect calls is now supported within kernel, and not only by the WP plug-in.


  • remove (almost unused) support for LTL and Promela as input language.
  • support for programs with indirect calls if they are annotated with calls annotations.


  • add support for logic functions returning a rational number.


  • 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.


  • 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.