|
|
# Frama-C release 20.0-beta (Calcium)
|
|
|
## Sources
|
|
|
- [frama-c-20.0-beta-Calcium.tar.gz](downloads/frama-c-20.0-beta-Calcium.tar.gz)
|
|
|
|
|
|
## Manuals
|
|
|
- [user-manual](manuals/user-manual-20.0-beta-Calcium.pdf)
|
|
|
- [acsl-implementation](manuals/acsl-implementation-20.0-beta-Calcium.pdf)
|
|
|
- [eva-manual](manuals/eva-manual-20.0-beta-Calcium.pdf)
|
|
|
- [plugin-development-guide](manuals/plugin-development-guide-20.0-beta-Calcium.pdf)
|
|
|
- [rte-manual](manuals/rte-manual-20.0-beta-Calcium.pdf)
|
|
|
- [wp-manual](manuals/wp-manual-20.0-beta-Calcium.pdf)
|
|
|
- [metrics-manual](manuals/metrics-manual-20.0-beta-Calcium.pdf)
|
|
|
- [aorai-manual](manuals/aorai-manual-20.0-beta-Calcium.pdf)
|
|
|
- [e-acsl-manual](manuals/e-acsl-manual-20.0-beta-Calcium.pdf)
|
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation-20.0-beta-Calcium.pdf)
|
|
|
- [e-acsl](manuals/e-acsl-1.14.pdf)
|
|
|
|
|
|
## Main changes (full Changelog is [here](https://git.frama-c.com/pub/frama-c/blob/20.0/Changelog))
|
|
|
|
|
|
### Kernel
|
|
|
|
|
|
- the minimum required OCaml version is now 4.05.0
|
|
|
- more strict checks related to ghost variables in non-ghost code, and support for ghost parameters
|
|
|
- (developer-only) visitor behavior functions were moved from `Cil` to a new module `Visitor_behavior`
|
|
|
|
|
|
### Eva
|
|
|
|
|
|
- New octagon domain inferring relations of the form
|
|
|
a ≤ ±X±Y ≤ b between pairs of integer variables X and Y.
|
|
|
- New option `-eva-auto-loop-unroll <N>`, to unroll all
|
|
|
loops whose number of iterations can be easily bounded by `<N>`.
|
|
|
- Dynamic registration of abstract values and domains:
|
|
|
developers of new domains no longer need to modify Eva's engine.
|
|
|
|
|
|
### WP
|
|
|
|
|
|
- Use native Why3 API (now requires why3 at compile time); deprecated native alt-ergo & coq output
|
|
|
- New cache mechanism for why3 provers, see `-wp-cache` option
|
|
|
|
|
|
### E-ACSL
|
|
|
|
|
|
- Support of rational numbers and operations.
|
|
|
|
|
|
### MdR
|
|
|
- new plug-in, Markdown-report, to generate reports in both Markdown and SARIF formats. |