package lreplay

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](https://dune.build/) >= 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