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:
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 installDepending of your system and your Frama-C installation, the latter command may need to be run as root or sudo-ed.
-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)To start detecting infeasible (or uncoverable) labels simply run:
frama-c -luncov-eva file.c -main funwhere 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).
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.cLabel 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 overflowYou 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.
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 WPparam: 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 WPfunction: information at each instruction to WPall: all of the aboveLUncov 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.cframa-c -luncov-value -luncov-debug 1 test.cAlso many thanks to the rest of LTest's team: