Merge branch 'ltest' into 'master'

Introducing LTest

See merge request !145

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