Skip to content
GitLab
26.0 protected
7d685b17 · Fixes a minor typo in the main changes for the 26.0 release. ·
Release Frama-C 26.0 Iron

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