LTest

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 to generate such a suite.

These three tools are available on Frama-C’s gitlab server under LGPL-2.1-only: - LAnnotate - LUncov - 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
• 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

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
• LUncov
• LReplay

They require OCaml>= 4.13.1, and, for the plugins, Frama-C 29.0 (Copper).