framac-19.0.md

---
layout: default
date: 21-06-2019
title: Release of Frama-C 19.0 (Potassium)
---

Frama-C 19.0 (Potassium) is out. Download it [here](/fc-versions/potassium.html).

Main changes with respect to Frama-C 18 (Argon) include:

#### Kernel:
- new check annotation, similar to assert except that it does not introduce
  additional hypotheses on the program state
- new options added to frama-c-script

#### GUI:
- compatibility with lablgtk3

#### Eva:
- New annotation "//@ split exp" to separate the analysis states for each
  possible value of an expression until a "//@ merge exp" annotation.
- New option -eva-partition-history to delay the join of the analysis states at
  merging points; useful when a reasoning depends on the path taken to reach a
  control point.
- By default, prints a summary at the end of the analysis.
- New meta option -eva-precision to globally configure the analysis.
- Improved precision on nested loops.

#### WP:
- new auto-search mode to automatically apply strategies and tactics (see -wp-auto)
- extended simplifications on range, bitwise and C-boolean values (_Bool is now
  handled by default)
- refactored float model (although it still requires further axiomatisation)

#### E-ACSL:
- support for user-defined logic functions and predicates without labels
- new option -e-acsl-functions that allows the user to specify a white/black list
  of functions in which annotations are monitored, or not.

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