Main changes since 25.0 Manganese
The Frama-C build now uses dune. Hopefully, this should have no impact on most
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).
callsACSL 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
- 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.