package frama-c-luncov
Luncov plugin of Frama-C, part of the LTest suite
Install
Dune Dependency
Authors
Maintainers
Sources
luncov-0.2.1.tar.bz2
md5=6c17a9c992ec04d6f9f2c6a7c97b0e71
sha512=243b617a27360379c80447e4e22b9393c966584ddfe245863f906ea876c31d492605ed2d47ecaabf17f81721c75face267fe3ef3dbf1fbc623177b3912fb6705
Description
Luncov is a plugin that attempts to identify unreachable and/or redundant tests objectives, represented in the code by labels and hyperlabels, as defined in the LTest family of Frama-C plug-ins. Other plug-ins in LTest include:
- Lannotate, for introducing (hyper)labels according to various criteria
- Lreplay, for executing a test suite and computing its coverage status
README
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page