|
|
# Frama-C release 26.0 (Iron)
|
|
|
## Sources
|
|
|
- [frama-c-26.0-Iron.tar.gz](https://www.frama-c.com/download/frama-c-26.0-Iron.tar.gz)
|
|
|
|
|
|
## Manuals
|
|
|
- [acsl](https://www.frama-c.com/download/acsl-1.18.pdf)
|
|
|
- [acsl-implementation](https://www.frama-c.com/download/acsl-implementation-26.0-Iron.pdf)
|
|
|
- [aorai-manual](https://www.frama-c.com/download/aorai-manual-26.0-Iron.pdf)
|
|
|
- [e-acsl](https://www.frama-c.com/download/e-acsl/e-acsl-1.18.pdf)
|
|
|
- [e-acsl-implementation](https://www.frama-c.com/download/e-acsl/e-acsl-implementation-26.0-Iron.pdf)
|
|
|
- [e-acsl-manual](https://www.frama-c.com/download/e-acsl/e-acsl-manual-26.0-Iron.pdf)
|
|
|
- [eva-manual](https://www.frama-c.com/download/eva-manual-26.0-Iron.pdf)
|
|
|
- [metrics-manual](https://www.frama-c.com/download/metrics-manual-26.0-Iron.pdf)
|
|
|
- [plugin-development-guide](https://www.frama-c.com/download/plugin-development-guide-26.0-Iron.pdf)
|
|
|
- [rte-manual](https://www.frama-c.com/download/rte-manual-26.0-Iron.pdf)
|
|
|
- [user-manual](https://www.frama-c.com/download/user-manual-26.0-Iron.pdf)
|
|
|
- [wp-manual](https://www.frama-c.com/download/wp-manual-26.0-Iron.pdf)
|
|
|
|
|
|
## Companion archives
|
|
|
- [aorai-example](https://www.frama-c.com/download/aorai-example-26.0-Iron.tar.gz)
|
|
|
- [hello](https://www.frama-c.com/download/hello-26.0-Iron.tar.gz)
|
|
|
|
|
|
## Main changes
|
|
|
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. |