From 5243d2517ac5fb438f0eb667de8f8b0e4b11bac9 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 22 Feb 2018 09:01:51 +0100
Subject: [PATCH] [userman] refer to undefined behavior detection in the
introduction
---
.../e-acsl/doc/userman/introduction.tex | 20 +++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index e3a2edf31ce..bad13d56f7d 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -13,16 +13,16 @@ program.
\eacsl translation brings several benefits. First, it allows a user to monitor
\C code and perform what is usually referred to as ``runtime assertion
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
- annotation checking'' would be more precise.}. This is the
-primary goal of \eacsl. Second, it allows to combine \framac and its
-existing analyzers with other \C analyzers that do not natively understand the
-\acsl
-specification language. Third, the possibility to detect invalid annotations
-during a concrete execution may be very helpful while writing a correct
-specification of a given program, \emph{e.g.} for later program proving.
-Finally, an executable specification makes it possible to check assertions that
-cannot be verified statically and thus to establish a link between
-runtime monitoring and static analysis tools such as
+ annotation checking'' would be more precise.}. This is the primary goal of
+\eacsl. Indirectly, in combination with the \rte~\cite{rte}, this usage
+allows the user to detect undefined behaviors in its \C code. Second, it allows
+to combine \framac and its existing analyzers with other \C analyzers that do
+not natively understand the \acsl specification language. Third, the possibility
+to detect invalid annotations during a concrete execution may be very helpful
+while writing a correct specification of a given program, \emph{e.g.} for later
+program proving. Finally, an executable specification makes it possible to
+check assertions that cannot be verified statically and thus to establish a link
+between runtime monitoring and static analysis tools such as
\valueplugin~\cite{value}\index{Value} or \wpplugin~\cite{wp}\index{Wp}.
Annotations used by the plug-in must be written in the \eacsl specification
--
GitLab