README.markdown

Frama-C/LTest: LReplay

Test replay and label coverage reporting tool

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. LReplay is the module of LTest in charge of replaying test cases and collecting coverage data.

Installation

LReplay requires OCaml 4.08.1 to be installed, as well as dune >= 3. To compile and install the executable, do

dune build
dune install

The latter command installs a single executable lreplay. It may be required to run it as root or to be sudo-ed. Classic Makefile options (prefix and bindir) may be defined to change the installation directory. For instance:

make bindir=~/bin install

will install the lreplay binary in the user's bin directory.

Usage

lreplay file.c [-update|-check|-init|-stats] [-drivers PATH] [-main FUN] [-force]

Mode

LReplay supports the following four modes:

• -update (the default)

  Computes label coverage given the test drivers and updates the FILE.labels file. Also shows some statistics about the coverage. The -force option may be used to force the re-compilation and re-execution of the test drivers.

• -check

  Computes label coverage given the test drivers and checks that FILE.labels already contains the correct information (for instance, to check the test generator outputs). Likewise -force may be used.

• -init

  Initializes the FILE.labels file by parsing FILE.c for labels. The -force option maybe used to overwrite the existing FILE.labels.

• -stats

  Shows some statistics about the coverage (by reading FILE.labels).

Drivers (for -update and -check)

Test drivers are specified with two options -drivers and -main.

The key option is -drivers. It specifies a pattern to find test drivers. The pattern may contain shell-like wildcards *, ?, [...], and variables of the form ${NAME} where NAME is one of SOURCE, DIRNAME, BASENAME, BASENAME_NO_EXT, and MAINFUN. The default value is specific to PathCrawler:

${DIRNAME}/testcases_${BASENAME_NO_EXT}/${MAINFUN}/testdrivers/TC_*.c.

The MAINFUN variable indicates the function under test (-main in Frama-C). By default it's set to *, that is every possible function for which PathCrawler had been run (in most cases, only one). You may change it via the -main flag.

LReplay can be used to run test suites that are not generated by PathCrawler, assuming that each test case comes with a driver. Here a driver is a C file that includes the annotated source file and contains a main function that calls the function under test on some test input data. So, if the drivers of a source file file.c are in a directory testcases, one could relay the tests and collect coverage as follows:

lreplay file.c -drivers 'testcases/*.c'

Authors

• Mickaël Delahaye
• Omar Chebaro
• Nikolai Kosmatov
• Sébastien Bardin
• Michaël Marcozzi
• Thibault Martin