package frama-c-luncov

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 uncoverable) 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 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 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