Frama C 20.0 beta Calcium

Frama-C release 20.0-beta (Calcium)

Sources

• frama-c-20.0-beta-Calcium.tar.gz

Manuals

• user-manual
• acsl-implementation
• eva-manual
• plugin-development-guide
• rte-manual
• wp-manual
• metrics-manual
• aorai-manual
• e-acsl-manual
• e-acsl-implementation
• e-acsl

Main changes (full Changelog is here)

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.