diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md new file mode 100644 index 0000000000000000000000000000000000000000..1ecaa317bee6d385e63b3956586ec2703122abaa --- /dev/null +++ b/_fc-plugins/ltest.md @@ -0,0 +1,62 @@ +--- +layout: plugin +title: LTest +description: Set of utilities for test coverage +key: reporting +distrib_mode: free +--- + +## Overview + +LTest is composed of two Frama-C plugins, `LAnnotate` and `LUncov`, +and one external executable, `LReplay`, that aim at providing +accurate test coverage metrics for a wide range of coverage criteria. + +More specifically, they are based on _labels_ and _hyperlabels_, +which formalize the notion of _test objectives_ that must be +covered for a given criterion. In this context, + +- `LAnnotate` generates the set of (hyper)labels corresponding to + the selected criteria for a given C program; +- `LUncov` attempts to detect the (hyper)labels that are uncoverable, + and the ones that are redundant; +- `LReplay` executes a test suite over some code instrumented with + (hyper)labels and computes a coverage ratio. + +On the other hand, these components, and notably `LReplay` assume that you +already have a test suite whose coverage you want to evaluate. Still in the +context of Frama-C, you can for instance use +[PathCrawler]({% link _fc-plugins/pathcrawler.md %}) to generate such a suite. + +These three tools are available on Frama-C's gitlab server under LGPL-2.1-only: +- [LAnnotate](https://git.frama-c.com/pub/ltest/lannotate) +- [LUncov](https://git.frama-c.com/pub/ltest/luncov) +- [LReplay](https://git.frama-c.com/pub/ltest/lreplay) + + +## Further Reading + +- Sébastien Bardin, Nikolai Kosmatov, Michaël Marcozzi, and Mickaël Delahaye. + _Specify and Measure, Cover and Reveal: A Unified Framework for Automated Test Generation._ + In _Science of Computer Programming_, 2021, vol. 207, ISSN 0167-6423. + [DOI: 10.1016/j.scico.2021.102641](https://doi.org/10.1016/j.scico.2021.102641) +- Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov and Virgile Prevosto. + _Generic and Effective Specification of Structural Test Objectives._ + In _Proc. of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)_, Tokyo, Japan, March 2017, pages 436-441. IEEE. ISBN 978-1-5090-6031-3. + [DOI: 10.1109/ICST.2017.57](https://doi.org/10.1109/ICST.2017.57) + +## Installation + +All three packages are available in `opam` and can be installed through + +``` +opam install frama-c-lannotate frama-c-luncov lreplay +``` + +Manual installation instructions are available in the README of each of the repositories: + +- [LAnnotate](https://git.frama-c.com/pub/ltest/lannotate/-/blob/master/README.markdown) +- [LUncov](https://git.frama-c.com/pub/ltest/luncov/-/blob/master/README.markdown) +- [LReplay](https://git.frama-c.com/pub/ltest/lreplay/-/blob/master/README.markdown) + +They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 (Chromium).