Blog

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 sake. Whatever the reason,...

Read More

Admit and check annotations in ACSL
André Maroneze on 10 June 2021

In Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to complement assert: the admit and check annotations. In a nutshell, assert P is equivalent to check P; admit P. The former allows easier checking of the validity of predicates, while the latter documents the introduction of external...

Read More

Frama-C GUI on the browser, via Docker
André Maroneze on 16 March 2021

New Frama-C Docker images, with a graphical interface, are available in the Docker Hub. They allow running Frama-C via a browser, on Windows, macOS and Linux. Frama-C + Docker + noVNC = Frama-C GUI on a browser The “traditional” Frama-C Docker images available on Docker Hub lack the graphical interface,...

Read More