package frama-c-luncov

  1. Overview
  2. Docs
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

Tags

software testing Frama-C LTest

Published: 09 Jul 2024

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

Dependencies (4)

  1. frama-c >= "29.0~" & < "30.0~"
  2. menhir build
  3. dune >= "3.7" & != "3.13.0"
  4. ocaml >= "4.13.1"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.