Skip to content
Snippets Groups Projects

Introducing LTest

Merged Virgile Prevosto requested to merge ltest into master
All threads resolved!
+ 62
0
---
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).
Loading