package lreplay

README.markdown

##########################################################################
#                                                                        #
#  This file is part of LReplay.                                         #
#                                                                        #
#  Copyright (C) 2007-2020                                               #
#    CEA (Commissariat à l'énergie atomique et aux énergies              #
#         alternatives)                                                  #
#                                                                        #
#  you can redistribute it and/or modify it under the terms of the GNU   #
#  Lesser General Public License as published by the Free Software       #
#  Foundation, version 2.1.                                              #
#                                                                        #
#  It is distributed in the hope that it will be useful,                 #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
#  GNU Lesser General Public License for more details.                   #
#                                                                        #
#  See the GNU Lesser General Public License version 2.1                 #
#  for more details (enclosed in the file licenses/LGPLv2.1).            #
#                                                                        #
##########################################################################

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 define to change the
installation directory. For instance:

    make bindir=~/bin install

will install the `lreplay` binary into the user 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 the label coverage given the test drivers and updates the
    `FILE.labels` file. Also show 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 the label coverage given the test drivers and checks that the
    `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`

    Show 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 `*`, `?`, `[...]` like the shell, 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 case, only one). You may change it via the `-main` flag.

LReplay can be use to run test suites that are not generated by PathCrawler,
assuming that each test case comes 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 some
source file `file.c` are in some 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