package frama-c-lannotate
Lannotate plugin of Frama-C, part of the LTest suite
Install
Dune Dependency
Authors
Maintainers
Sources
lannotate-0.2.3.tar.bz2
md5=93f0b2ec2c39599b70bb4f2d504ab817
sha512=1682fddf70d90db51bf8fbfa688fb6a898f779e720cccc064298665d34dab2960c8b621abf1ee9bdd0117759f4c5a3def8d689edd10549fc7440edaba1730d96
Description
Lannotate is a plugin that introduces labels and hyperlabels formalizing test objectives corresponding to the coverage criteria selected by the user. It is part of LTest, a set of plug-in dedicated to managing test coverage. Other plug-ins in LTest include:
- Luncov, for detecting polluting (infeasible or redundant) objectives
- Lreplay, for executing a test suite and computing its coverage status
README
README.markdown
Frama-C/LTest: LAnnotate
========================
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. *LAnnotate* is the module of LTest in charge of adding coverage
objectives into program in the form of annotations.
LAnnotate is a Frama-C plugin.
Installation
------------
LAnnotate requires Frama-C 24.0 (Chromium) to be installed and OCaml >= 4.08.1 .
Once Frama-C is installed, run autoconf, configure, compile and install
LAnnotate:
autoconf
./configure
make
make install
The last command may need to be run as root (or sudo) depending on your
Frama-C installation.
Usage
-----
frama-c -lannot=CRITERIA file.c
where CRITERIA is a comma-separated list of criteria. It outputs a new
annotated file named `file_labels.c`, with labels for each selected criterion.
Implemented criteria are DC, CC, MCC, n-CC, GACC, GICC, WM, IDP and FC.
for more information, run `frama-c -lannot-list` and see the [criteria
documentation](doc/criteria.markdown).
Global options are :
- `-lannot-simplify` enables the simplication of the generated label
predicates before annotations. For the moment, it only reduces Boolean
expressions.
- `-lannot-allbool` tells LAnnotate to consider all Boolean expressions,
rather that just branching decisions. Impacts DC, CC, MCC, n-CC, GACC, GICC.
- `-lannot-functions funs` tells LAnnotate which functions to consider
(all by default).
- `-lannot-o outputfile.c` tells LAnnotate how to name the annoted file
(by default, add `_labels` before the extension).
There exist other options that are specific to some criteria, see the criteria
doc. To get the full list of options, run `frama-c -lannot-help`.
Authors
-------
- Omar Chebaro
- Mickaël Delahaye
- Michaël Marcozzi
- Thibault Martin
Also many thanks to the rest of LTest's team:
- Nikolai Kosmatov
- Sébastien Bardin
On This Page