Introducing LTest

_fc-plugins/ltest.md

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