LTest is composed of two Frama-C plugins,
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,
LAnnotategenerates the set of (hyper)labels corresponding to the selected criteria for a given C program;
LUncovattempts to detect the (hyper)labels that are uncoverable, and the ones that are redundant;
LReplayexecutes 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.
- 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
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:
They require OCaml>= 4.08.1, and, for the plugins, Frama-C 24.0 (Chromium).