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.
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.