diff --git a/_posts/2022-04-19-ltest-plugins-released.md b/_posts/2022-04-19-ltest-plugins-released.md new file mode 100644 index 0000000000000000000000000000000000000000..48bb47026fe570574cba325dff09ca8f87488666 --- /dev/null +++ b/_posts/2022-04-19-ltest-plugins-released.md @@ -0,0 +1,51 @@ +--- +layout: post +author: André Maroneze (review by Virgile Prevosto) +date: 2022-04-19 12:00 +0100 +categories: test +title: "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](https://git.frama-c.com/pub/ltest), +and as 3 opam packages: +[frama-c-luncov](https://opam.ocaml.org/packages/frama-c-luncov/), +[frama-c-lannotate](https://opam.ocaml.org/packages/frama-c-lannotate/), +and [lreplay](https://opam.ocaml.org/packages/lreplay/). + +These plugins help measure test coverage based on *hyperlabels*. +Details about them are published +[here](http://sebastien.bardin.free.fr/final-SCP-2021.pdf) and +[here](http://sebastien.bardin.free.fr/2017-icst-tool.pdf) +(you can also see the +[LTest plugin page on the Frama-C website](https://www.frama-c.com/fc-plugins/ltest.html)). + +Note that these plugins do not help generating test cases; +for that, you may want to use +[PathCrawler](https://www.frama-c.com/fc-plugins/pathcrawler.html) +(not open-source). + +## A bit of history + +The LTest plugin is not new: it +[has been released several years ago](https://micdel.fr/ltest.html), +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](https://github.com/ltest-dev/LTest), 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](https://www.frama-c.com/fc-plugins/pathcrawler.html), +but it can be configured for use with other test generators.