---
layout: plugin
title: RTE
description: Generates annotations for possible runtime errors and other properties.
key: specifications
distrib_mode: main
manual_pdf: /download/rte-manual.pdf
---

## 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](wp.html) or [E-ACSL](e-acsl.html) plug-ins, which will be used to
verify that the assertions are valid (hence, that no runtime errors can occur).

Note that the [Eva](eva.html) 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](eva.html) 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.