Test plug-ins (re-)released: LUncov, LAnnotate, LReplay (all part of LTest)

André Maroneze (review by Virgile Prevosto) - 19th Apr 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 plugin page on the Frama-C website).

Note that these plugins do not help generating test cases; for that, you may want to use PathCrawler (not open-source).

A bit of history

The LTest plugin is not new: it has been released several years ago, as part of Mickaël Delahaye’s PhD. However, that version (compatible with a patched version of Frama-C Neon) has aged a bit, making it hard for users to get it working with recent Frama-C versions. Other releases were made on Github, usually related to published papers, but once again, their maintenance was sporadic. This opam release, plus the code being kept closer to Frama-C’s development version in Gitlab, should help keep these plug-ins relevant. Note that the released version is numbered 0.1, which indicates that they are still in an experimental stage; industrial users should contact the Frama-C team for details about their maturity.

You may also have noticed: why is the opam package for LReplay named lreplay and not frama-c-lreplay? The simple reason is that, unlike the others, it is not a Frama-C plug-in per se, but an independent tool (it even has its own Dune build file) that can be used with or without Frama-C. It turns out that its defaults are mostly tuned for using it in conjunction with PathCrawler, but it can be configured for use with other test generators.

André Maroneze (review by Virgile Prevosto)
19th Apr 2022