Commit 5243d251 authored by Julien Signoles's avatar Julien Signoles
Browse files

[userman] refer to undefined behavior detection in the introduction

parent 101ef9f0
...@@ -13,16 +13,16 @@ program. ...@@ -13,16 +13,16 @@ program.
\eacsl translation brings several benefits. First, it allows a user to monitor \eacsl translation brings several benefits. First, it allows a user to monitor
\C code and perform what is usually referred to as ``runtime assertion \C code and perform what is usually referred to as ``runtime assertion
checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
annotation checking'' would be more precise.}. This is the annotation checking'' would be more precise.}. This is the primary goal of
primary goal of \eacsl. Second, it allows to combine \framac and its \eacsl. Indirectly, in combination with the \rte~\cite{rte}, this usage
existing analyzers with other \C analyzers that do not natively understand the allows the user to detect undefined behaviors in its \C code. Second, it allows
\acsl to combine \framac and its existing analyzers with other \C analyzers that do
specification language. Third, the possibility to detect invalid annotations not natively understand the \acsl specification language. Third, the possibility
during a concrete execution may be very helpful while writing a correct to detect invalid annotations during a concrete execution may be very helpful
specification of a given program, \emph{e.g.} for later program proving. while writing a correct specification of a given program, \emph{e.g.} for later
Finally, an executable specification makes it possible to check assertions that program proving. Finally, an executable specification makes it possible to
cannot be verified statically and thus to establish a link between check assertions that cannot be verified statically and thus to establish a link
runtime monitoring and static analysis tools such as between runtime monitoring and static analysis tools such as
\valueplugin~\cite{value}\index{Value} or \wpplugin~\cite{wp}\index{Wp}. \valueplugin~\cite{value}\index{Value} or \wpplugin~\cite{wp}\index{Wp}.
Annotations used by the plug-in must be written in the \eacsl specification Annotations used by the plug-in must be written in the \eacsl specification
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment