Runtime error annotation generation plug-in

The runtime error annotation plug-in Rte allows the generation of annotations for:

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

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.

User Manual

RTE plug-in Manual.