From 7eb472b7e5f5093387802012a26a68aeeb309e3c Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 18 Sep 2018 17:56:35 +0200
Subject: [PATCH] [userman] improve intro
---
src/plugins/e-acsl/doc/userman/biblio.bib | 20 +++++++++++++
.../e-acsl/doc/userman/introduction.tex | 30 +++++++++++--------
2 files changed, 38 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 3a444b97790..3b4015a6d13 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -49,6 +49,26 @@
note = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
}
+@habilitation{signoles18hdr,
+ author = {Signoles, Julien},
+ title = {{From Static Analysis to Runtime Verification with Frama-C and E-ACSL}},
+ year = 2018,
+ month = jul,
+ school = {Universit\'e Paris-Sud, Orsay, France},
+ note = {Habilitation Thesis},
+ url = {publis/hdr.pdf}
+}
+
+@inproceedings{rvcubes17tool,
+ author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
+ title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
+Programs. Tool Paper}},
+ booktitle = {International Workshop on Competitions, Usability, Benchmarks,
+Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)},
+ year = 2017,
+ month = sep,
+}
+
@inproceedings{sac13,
author = {Micka\"{e}l Delahaye and Nikolai Kosmatov and Julien Signoles},
title = {Common Specification Language for Static and Dynamic Analysis of
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 03e8b405449..0a891902150 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -14,22 +14,28 @@ program.
\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. 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
-\Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}.
+\eacsl. Indirectly, in combination with plug-in \rte~\cite{rte} of \framac, 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 \Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}.
Annotations used by the plug-in must be written in the \eacsl specification
language~\cite{eacsl,sac13} -- a subset of \acsl. \eacsl plug-in is still in a
preliminary state: some parts of the \eacsl specification language are not yet
-supported. Annotation supported by the plugin are described in a separate
-document~\cite{eacsl-implem}.
+supported. Annotations supported by the plugin are described in a separate
+document~\cite{eacsl-implem}. It is worth noting that the annotations that aim
+to be dynamically verified are not necessarily hand-written, but may be
+automatically generated instead. That is for instance the case when checking the
+absence of undefined behaviors in combination with RTE, as mentionned in the
+previous paragraph. Using \eacsl this way is therefore a fully automatic
+process. Many usages, including automatic usages, are described in companion
+research papers~\cite{rv13tutorial,rvcubes17tool,signoles18hdr}.
This manual does \emph{not} explain how to install the \eacsl plug-in. For
installation instructions please refer to the \texttt{INSTALL} file in the
--
GitLab