Frama-C release 20.0-beta (Calcium)
here)Main changes (full Changelog is
- 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
Cilto a new module
- 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
- Dynamic registration of abstract values and domains: developers of new domains no longer need to modify Eva's engine.
- Use native Why3 API (now requires why3 at compile time); deprecated native alt-ergo & coq output
- New cache mechanism for why3 provers, see
- Support of rational numbers and operations.
- new plug-in, Markdown-report, to generate reports in both Markdown and SARIF formats.