RTE

rte.html

+---
+layout: plugin
+title: RTE
+description: Runtime Time Error
+key: specifications
+---
+
+<dl class="defnitionList">
+  <dt class="subTitle">Overview</dt>
+  <dd><p>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 <a href="wp.html">Wp</a> or
+      <a href="e-acsl.html">E-ACSL</a> plug-ins, that will be used to verify
+      that the assertions are valid (hence that no runtime error can occur).
+      It is not necessary to use RTE together with
+      the <a href="eva.html">Eva</a> plug-in, as the latter already generate
+      an alarm and the corresponding assertion if it cannot guarantee that
+      evaluating a given expression is always safe.
+    </p>
+  </dd>
+  <dt class="subTitle">Use</dt>
+  <dd>
+    <p>RTE is part of the main distribution of Frama-C. It is
+      activated with the <tt>-rte</tt> option. It is possible to
+      select only specific kinds of runtime errors with the <tt>-warn-*</tt>
+      options of Frama-C's kernel (by default all categories are activated).
+    </p>
+  </dd>
+</dl>