---
layout: default
date: 04-12-2019
title: Release of Frama-C 20.0 (Calcium)
---

Frama-C 20.0 (Calcium) is out. Download it [here](/fc-versions/calcium.html).

Main changes with respect to Frama-C 19 (Potassium) include:

##### 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
  - 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.

And a new plug-in, Markdown-report (MdR), to generate reports in both Markdown and SARIF formats.

A complete changelog can be found [here](/html/changelog.html#Calcium-20.0).