Blog

E-ACSL now works in Frama-C Docker images
André Maroneze on 20 December 2022

The Frama-C Docker images available on Docker Hub were based on Alpine Linux, which allows for minimal sizes. However, its reliance on musl instead of the GNU libc (present in most Linux distributions) led to incompatibility issues with the E-ACSL plug-in. For this reason, current and future Docker images will...

Read More

Frama-C 26 (Iron): a release with several irons in the fire
André Maroneze (reviewed by David Bühler, Valentin Perrelle) on 29 November 2022

Frama-C 26 (Iron) has been released, and as always, it contains several improvements among different plug-ins. In this blog post, we will present some of them, with very short examples. This list of features is based on the main changes since the 25.0 (Manganese) release. Kernel/Aoraï: ‘calls’ ACSL extension moved...

Read More

SuperTest and Frama-C: a Clash of Titans
A. Maroneze (Frama-C), V. Yaglamunov & M. Beemster (Solid Sands) on 16 November 2022

This post has been co-written with Solid Sands; it is also available at the Solid Sands blog. Some time ago, the Frama-C team entered into a partner agreement with Solid Sands to make use of SuperTest, a very thorough test suite for C compilers and libraries. From basic syntactic tests...

Read More

Frama-C 25 includes a preview version of Ivette, the new Frama-C GUI
André Maroneze (review by David Bühler) on 12 July 2022

The Frama-C GUI, based on GTK, is undergoing a retirement process; Ivette, the new graphical interface, will replace it in a few versions. The first public preview of Ivette has shipped with Frama-C 25.0 (Manganese). This post will briefly present how to compile and run it. It also illustrates some...

Read More

Test plug-ins (re-)released: LUncov, LAnnotate, LReplay (all part of LTest)
André Maroneze (review by Virgile Prevosto) on 19 April 2022

The Ltest “meta-plugin” (composed of three parts: LUncov, LAnnotate and LReplay) has been (re-)released on Frama-C’s public Gitlab, and as 3 opam packages: frama-c-luncov, frama-c-lannotate, and lreplay. These plugins help measure test coverage based on hyperlabels. Details about them are published here and here (you can also see the LTest...

Read More