Blog

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

Quick ACSL Guide for Eva: a new mini-tutorial
André Maroneze (review by V. Prevosto, P. Baudin) on 6 April 2022

In 2016, a few blog posts (part 1, part 2, part 3) presented a short tutorial on writing ACSL clauses for Eva (back then, the Value Analysis plug-in). A few things changed since then, but posting them again in this blog would lead to the same issue in the future....

Read More

Running old Frama-C versions from Docker images
André Maroneze on 15 October 2021

There are several reasons one might want to run an old version of Frama-C: - to test some outdated plugin which is only compatible with a previous version; - to re-run analyses mentioned in an old tutorial or blog post; - to compare results between Frama-C versions; - for nostalgia’s...

Read More