package lreplay

  1. Overview
  2. Docs
Executes a test suite and computes test coverage


Dune Dependency






Lreplay is part of the LTest suite, which includes tools to manage test objectives, expressed as labels and hyperlabels. lreplay runs a given test suite and computes the corresponding coverage according the labels and hyperlabels defined in its input files. The other LTest tools are Frama-C plugins including:

  • Lannotate, for generating (hyper)labels according to various criteria
  • Luncov, for identifying uncoverable and/or redundant (hyper)labels

Published: 09 Jul 2024



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.

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.


    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:


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'


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

Dependencies (4)

  1. menhir build & >= "20180528"
  2. dune >= "3.7" & != "3.13.0"
  3. ocaml >= "4.13.1"
  4. base-unix

Dev Dependencies (1)

  1. odoc with-doc

Used by





Innovation. Community. Security.