Runtime error annotation generation plug-in
The runtime error annotation plug-in Rte allows the generation of annotations for:
- common runtime errors (see annex undefined behaviors of ISO C99 draft version )
- overflows on unsigned integer operations (which is a well-defined behavior)
- function contracts inlining at call sites
The annotations generated by the Rte plug-in can later be discharged by more advanced plug-ins such as Jessie and Wp. The reader should be aware that discharging such annotations is much more difficult than simply generating them, and that there is no guarantee that a plug-in such as Value analysis will be able to do so automatically in all cases.
Usage
A typical command line usage has the form
frama-c -rte file.c
or equivalently
frama-c -rte -rte-all file.c
This will enable generation of all possible annotations, except for those concerned with unsigned overflows, which are well-defined behaviors according to ISO C99.
For generating all possible annotations on all functions, including function contracts inlining, use:
frama-c -rte -rte-unsigned-ov file.c
By default, annotations are generated on the whole file. Use -rte-select to generate them on a set of functions:
frama-c -rte -rte-select f,g file.c
By default, most annotations are generated once -rte is set. To generate only a subset of annotations, use -rte-no-all in conjunction with specific generation options. For instance, the following command only generates function contracts inlining annotations:
frama-c -rte -rte-no-all -rte-precond file.c
Restrictions
- No contract is generated at call sites for functions called through pointers.
- Only a small subset of all possible undefined behaviors of ISO C99 are treated by Rte. For instance, no annotation is generated when comparing two pointers with a relational operator.
Plug-in Options
Global options:
- -rte
- Enable the plug-in.
- -rte-all
- Enable all runtime-errors annotations, except for unsigned overflows (see >-rte-unsigned-ov).
- -rte-const
- Generate status for annotation through constant folding.
- -rte-print
- Pretty-print the annotated code.
- -rte-warn
- Emit warning on broken annotations.
- -rte-select f1,...,fn
- Run plugin on a subset f1,...,fn of functions.
Runtime-error annotations options:
- -rte-unsigned-ov
- Generate annotations for unsigned overflows (not entailed by -rte).
- -rte-signed
- Generate annotations for signed overflows.
- -rte-downcast
- Generate annotations for signed integer downcast.
- -rte-div
- Generate annotations for division by zero.
- -rte-mem
- Generate annotations for validity of left-values access.
Contract annotations option:
- -rte-precond
- Generate contract-based statement behaviors based at call sites.