RTE

Overview

The RTE plug-in is dedicated to generate an ACSL assertion for each expression potentially leading to an undefined behavior (e.g. invalid pointer dereference, arithmetic overflow). It is usually used as a pre-processor for the Wp or E-ACSL plug-ins, which will be used to verify that the assertions are valid (hence, that no runtime errors can occur).

Note that the Eva plug-in already performs verification of runtime errors; it generates an alarm and the corresponding assertion, but only if it cannot guarantee that evaluating a given expression is always safe (for any concrete execution starting from an initial state included in the abstract initial state given to Eva). Therefore, combining Eva and RTE is unnecessary.

Usage

RTE is part of the main distribution of Frama-C. It is activated with the -rte option. It is possible to select only specific kinds of runtime errors with the -warn-* options of Frama-C’s kernel.