|
|
|
# Frama-C release 25.0~beta (Manganese)
|
|
|
|
## Sources
|
|
|
|
- [frama-c-25.0-beta-Manganese.tar.gz](downloads/frama-c-25.0-beta-Manganese.tar.gz)
|
|
|
|
|
|
|
|
## Manuals
|
|
|
|
- [acsl-1.18](manuals/acsl-1.18.pdf)
|
|
|
|
- [acsl-implementation](manuals/acsl-implementation-25.0-beta-Manganese.pdf)
|
|
|
|
- [aorai-example-25.0-beta-Manganese.tgz](manuals/aorai-example-25.0-beta-Manganese.tgz)
|
|
|
|
- [aorai-manual](manuals/aorai-manual-25.0-beta-Manganese.pdf)
|
|
|
|
- [e-acsl-1.18](manuals/e-acsl-1.18.pdf)
|
|
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation-25.0-beta-Manganese.pdf)
|
|
|
|
- [e-acsl-manual](manuals/e-acsl-manual-25.0-beta-Manganese.pdf)
|
|
|
|
- [eva-manual](manuals/eva-manual-25.0-beta-Manganese.pdf)
|
|
|
|
- [metrics-manual](manuals/metrics-manual-25.0-beta-Manganese.pdf)
|
|
|
|
- [plugin-development-guide](manuals/plugin-development-guide-25.0-beta-Manganese.pdf)
|
|
|
|
- [rte-manual](manuals/rte-manual-25.0-beta-Manganese.pdf)
|
|
|
|
- [user-manual](manuals/user-manual-25.0-beta-Manganese.pdf)
|
|
|
|
- [wp-manual](manuals/wp-manual-25.0-beta-Manganese.pdf)
|
|
|
|
|
|
|
|
## Main changes
|
|
|
|
### Kernel
|
|
|
|
- New `admit` annotations (which already accepted `assert` and `check`) to express hypotheses to be admitted but not verified by Frama-C
|
|
|
|
- Set default machdep to `x86_64`; allow setting machdep via environment variable FRAMAC_MACHDEP
|
|
|
|
|
|
|
|
### AORAI
|
|
|
|
|
|
|
|
- New option for tracking the last N states of the automaton. Easier analysis of instrumented code with Eva.
|
|
|
|
|
|
|
|
### E-ACSL
|
|
|
|
- Add runtime support for Windows
|
|
|
|
- Add support for loop variant
|
|
|
|
- Add support for multiple binders in guarded quantifications
|
|
|
|
|
|
|
|
### EVA
|
|
|
|
- Partial support for recursion: new option -eva-unroll-recursive-calls to
|
|
|
|
precisely analyze the n first recursive calls, before using the function
|
|
|
|
specification to interpret the remaining calls.
|
|
|
|
- Improved automatic widening thresholds
|
|
|
|
- Improved automatic loop unroll
|
|
|
|
|
|
|
|
### WP
|
|
|
|
- New internal WP engine, fixing many issues related to control flow graph and
|
|
|
|
local variable scoping. Support for stmt contracts has been removed. Support
|
|
|
|
for looping gotos has been removed. Altough unsound, the legacy engine is
|
|
|
|
still accessible via -wp-legacy option.
|
|
|
|
- Bump Why3 version to 1.4.0
|
|
|
|
- Section « Limitation & Roadmap » added to the WP manual. |
