framac-27.0-beta.md

layout: default
date: "16-05-2023"
short_title: Frama-C 27.0~beta (Cobalt)
title: Beta release of Frama-C 27.0~beta (Cobalt)
link: /fc-versions/cobalt.html

Frama-C 27.0~beta (Cobalt) is out. Download it here.

Main changes with respect to Frama-C 26.0 (Iron) include:

Kernel

• Supports C11 _Generic
• New machdep mechanism, based on YAML files
• New script for generating machdeps from a C11 compiler

Aoraï

• Supports specification about floating-point variables.

Eva

• The octagon domain can now infer relations between any lvalues of integer or pointer types.
• Fixes the bitwise domain on big-endian architectures.

WP

• Why3 version bumped to 1.6.0.
• New options for controlling goal automatic splitting
• Default timeout is now 2s

GTK GUI

• Removed GTK2 support

Ivette

• The Eva table can show the values of function parameters, the logical status of ACSL predicates, and the values of C lvalues in these predicates. It also shows the status of uninitialized and escaping variables.
• Information about C types are shown in the Inspector.
• Many bug fixes and user experience improvements.