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.
A typical command line usage has the form
frama-c -rte file.c
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
- 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.
- Enable the plug-in.
- Enable all runtime-errors annotations, except for unsigned overflows (see >-rte-unsigned-ov).
- Generate status for annotation through constant folding.
- Pretty-print the annotated code.
- Emit warning on broken annotations.
- -rte-select f1,...,fn
- Run plugin on a subset f1,...,fn of functions.
Runtime-error annotations options:
- Generate annotations for unsigned overflows (not entailed by -rte).
- Generate annotations for signed overflows.
- Generate annotations for signed integer downcast.
- Generate annotations for division by zero.
- Generate annotations for validity of left-values access.
Contract annotations option:
- Generate contract-based statement behaviors based at call sites.