diff --git a/_fc-plugins/ltest.md b/_fc-plugins/ltest.md new file mode 100644 index 0000000000000000000000000000000000000000..5dac5dcc394e87c4c00b598c1599e84269fe57f2 --- /dev/null +++ b/_fc-plugins/ltest.md @@ -0,0 +1,51 @@ +--- +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 formalizes 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 unreachable, + and the ones that are redundant; +- `LReplay` executes a test suite over some code instrumented with + (hyper)labels and computes a coverage ratio. + +## 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 trough + +``` +opam install frama-c-lannotate frama-c-luncov lreplay +``` + +Manual installation instructions are available in the README of each of the repositories: + +- [https://git.frama-c.com/pub/ltest/lannotate](https://git.frama-c.com/pub/ltest/lannotate) +- [https://git.frama-c.com/pub/ltest/luncov](https://git.frama-c.com/pub/ltest/luncov) +- [https://git.frama-c.com/pub/ltest/lreplay](https://git.frama-c.com/pub/ltest/lreplay) + +They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 Chromium