|
|
|
# Frama-C release 25.0 (Manganese)
|
|
|
|
## Sources
|
|
|
|
- [frama-c-25.0-Manganese.tar.gz](downloads/frama-c-25.0-Manganese.tar.gz)
|
|
|
|
|
|
|
|
## Manuals
|
|
|
|
- [acsl-1.18](manuals/acsl-1.18.pdf)
|
|
|
|
- [acsl-implementation](manuals/acsl-implementation-25.0-Manganese.pdf)
|
|
|
|
- [aorai-example-25.0-Manganese.tgz](manuals/aorai-example-25.0-Manganese.tgz)
|
|
|
|
- [aorai-manual](manuals/aorai-manual-25.0-Manganese.pdf)
|
|
|
|
- [e-acsl-1.18](manuals/e-acsl-1.18.pdf)
|
|
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation-25.0-Manganese.pdf)
|
|
|
|
- [e-acsl-manual](manuals/e-acsl-manual-25.0-Manganese.pdf)
|
|
|
|
- [eva-manual](manuals/eva-manual-25.0-Manganese.pdf)
|
|
|
|
- [metrics-manual](manuals/metrics-manual-25.0-Manganese.pdf)
|
|
|
|
- [plugin-development-guide](manuals/plugin-development-guide-25.0-Manganese.pdf)
|
|
|
|
- [rte-manual](manuals/rte-manual-25.0-Manganese.pdf)
|
|
|
|
- [user-manual](manuals/user-manual-25.0-Manganese.pdf)
|
|
|
|
- [wp-manual](manuals/wp-manual-25.0-Manganese.pdf)
|
|
|
|
|
|
|
|
## Main changes
|
|
|
|
### Kernel
|
|
|
|
|
|
|
|
- The experimental AST Diff module allows to compute difference between the AST
|
|
|
|
of two projects
|
|
|
|
- significant changes in AST types that might break existing development
|
|
|
|
|
|
|
|
### E-ACSL
|
|
|
|
|
|
|
|
- add support for Linux's pthread concurrency
|
|
|
|
|
|
|
|
### EVA
|
|
|
|
|
|
|
|
- New public API to run the analysis and access its results, intended to replace the old API in Db.Value.
|
|
|
|
- Improved multidim domain: it is now more precise and more robust, and is able to infer simple array invariants and disjunctive struct invariants.
|
|
|
|
|
|
|
|
### WP
|
|
|
|
|
|
|
|
- uses Why3 1.5.0
|
|
|
|
- new supported ACSL features : decreases clause and general measures for variant and decreases
|
|
|
|
- new tactics: Clear for hypothesis removal and ModMask for rewriting of mask and modulos
|
|
|
|
- removed deprecated legacy WP engine and native prover output (always use Why3)
|
|
|
|
- fixes loop invariant order and collect more hypotheses when proving them
|
|
|
|
|
|
|
|
### Ivette (New Frama-C GUI)
|
|
|
|
|
|
|
|
We are introducing Ivette, a new GUI for Frama-C.
|
|
|
|
In this preliminary version, only EVA and some of its derived plug-ins are supported.
|
|
|
|
|
|
|
|
Build & install instructions are in `ivette/INSTALL.md` from the source tarball.
|
|
|
|
To try it, simply use `ivette` in replacement of `frama-c-gui`.
|
|
|
|
Your feedback is welcome.
|
|
|
|
|
|
|
|
Have fun ! |
