package frama-c-luncov

README.markdown

Frama-C/LTest: LUncov
=====================
*Infeasible test requirement detection*

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. *LUncov* is the module of LTest in charge of detecting infeasible
(or *uncov*erable) test requirements. As the rest of the toolkit, this module
requires that your test requirements are encoded as labels.

LUncov is a Frama-C plugin.

LUncov offers three ways to detect infeasible requirements:

  - Evolved Value Analysis: global analysis, done only once for every label
  - Weakest precondition: done once per label
  - Their combination

Installation
------------

LUncov requires Frama-C 24.0 (Chromium) and OCaml 4.08.1 to be installed.
To install it run the following commands in LUncov's directory:

    autoconf
    ./configure
    make
    make install

Depending of your system and your Frama-C installation, the latter command may
need to be run as root or `sudo`-ed.

Usage
-----

### Three modes

  - `-luncov-eva` detects infeasible requirements by a
    global one-time analysis

  - `-luncov-wp` detects infeasible labels by a distinct
    analysis for each label

  - `-luncov-vwap` detects infeasible labels by combining
    a global analysis with a goal-oriented analysis
    (Deactivated for now, WIP)

### Running the detection

To start detecting infeasible (or uncoverable) labels simply run:

    frama-c -luncov-eva file.c -main fun

where `file.c` is the name of the file under test and `fun` is the name of the
function under test.

*N.B.* LUncov automatically updates (or creates one if missing) the label
coverage file (here `test.labels`).

### Value analysis (Eva)-based detection

You may specify Eva analysis' parameters. See `frama-c -eva-help` and/or
[Eva's manual](https://frama-c.com/download/frama-c-eva-manual.pdf) for
details. It may be useful to limit the verbosity of the analysis
(`-eva-verbose`), or to increase its precision, e.g.:

    frama-c -luncov-eva -eva-verbose 0 -eva-precision 4 test.c

Label pruning will be based on a more precise value analysis, with
`-eva-precision 4` instructing Eva to tune some parameters towards more
precision.

Other useful parameters include:

  - `-context-width n`  indicates Frama-C to use `n` as the width of the default
    context for value analysis (default: 2). Note that if the entry function
    takes a pointer to `t` as input Frama-C will considers that it points to an
    array of `t` whose size is `n`.

  - `-lib-entry` tells Frama-C to consider the entry function as a library call
    rather than a program main. In particular, when on, Frama-C considers that
    globals may have any value, instead of the ones they are initialized to.

  - `-no-warn-signed-overflow` to adopt two's complement as the semantics of
    integer signed overflow

### Weakest precondition (WP)-based detection

You may specify additional weakest precondition parameters. The most useful
parameter is without a doubt `-wp-model model` to choose the actual model used
by WP, for instance `typed` or `hoare` with options such as `int` (vs. `nat`) or
`cast`. Recommended value: `typed+int`.
See `frama-c -wp-help` or the
[WP manual](https://frama-c.com/download/frama-c-wp-manual.pdf) for details.

Note that LUncov considers each annotation already present in the code as valid.

### Hybrid approach: value analysis and weakest precondition

In addition to flags relevant to both approaches, the hybrid approach uses an
additional parameter `-luncov-strategy s`. Indeed, the hybrid approach
transfers some information computed by the value analysis to the weakest
precondition calculus. The strategy `s` specifies what information to
transfer. Accepted strategies are:

  - `none`: no information is provided to WP
  - `param`: information about function parameters
    (e.g. possible values of the parameters)
  - `label`: information about the label
    (e.g. possible values about the variable it uses)
  - `param+label`: function parameters are provided to WP
  - `function`: information at each instruction to WP
  - `all`: all of the above

### Label database initialization

LUncov assumes a label database is present. If you need to generate one from the
source file on-the-fly, simply add `-luncov-init` to the command line.
Alternatively, it can be run alone:

    frama-c -luncov-init myfile.c

### Debug info

    frama-c -luncov-value -luncov-debug 1 test.c

Authors
-------

  - Mickaël Delahaye
  - Robin David
  - Thibault Martin

Also many thanks to the rest of LTest's team:
  - Sébastien Bardin
  - Omar Chebaro
  - Nikolai Kosmatov