Frama-C/LTest (or LTest for short) is a generic and integrated toolkit for automation of white-box testing of C programs. This toolkit provides a unified support of many different testing criteria as well as an easy integration of new criteria. LAnnotate is the module of LTest in charge of adding coverage objectives into program in the form of annotations.
LAnnotate is a Frama-C plugin.
LAnnotate requires Frama-C 24.0 (Chromium) to be installed and OCaml >= 4.08.1 . Once Frama-C is installed, run autoconf, configure, compile and install LAnnotate: autoconf ./configure make make install
The last command may need to be run as root (or sudo) depending on your Frama-C installation.
frama-c -lannot=CRITERIA file.c
where CRITERIA is a comma-separated list of criteria. It outputs a new
annotated file named file_labels.c, with labels for each selected criterion.
Implemented criteria are DC, CC, MCC, n-CC, GACC, GICC, WM, IDP and FC.
for more information, run frama-c -lannot-list and see the criteria
documentation.
Global options are :
-
-lannot-simplifyenables the simplication of the generated label predicates before annotations. For the moment, it only reduces Boolean expressions. -
-lannot-allbooltells LAnnotate to consider all Boolean expressions, rather that just branching decisions. Impacts DC, CC, MCC, n-CC, GACC, GICC. -
-lannot-functions funstells LAnnotate which functions to consider (all by default). -
-lannot-o outputfile.ctells LAnnotate how to name the annoted file (by default, add_labelsbefore the extension).
There exist other options that are specific to some criteria, see the criteria
doc. To get the full list of options, run frama-c -lannot-help.
- Omar Chebaro
- Mickaël Delahaye
- Michaël Marcozzi
- Thibault Martin
Also many thanks to the rest of LTest's team:
- Nikolai Kosmatov
- Sébastien Bardin