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

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.