diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 3a444b97790c71379b9e33a1577d3fcb2aadd2d8..27d9be4791f802dbe9eebcb8cd3ed69c8cbe2139 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/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index af68ce7761da9682947653fd0e2f330612bdc8c9..b4969d93baf04103318d1bd47a19e72d38429763 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -3,9 +3,23 @@
This chapter summarizes the changes in this documentation between each \eacsl
release. First we list changes of the last release.
+\section*{E-ACSL \eacslversion}
+
+\begin{itemize}
+\item \textbf{Introduction}: Improve a bit and reference related papers.
+\item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
+ not yet robust.
+\item \textbf{What the Plug-in Provides}: Highlight the importance of
+ \textbf{-e-acsl-prepare}.
+\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
+ Monitoring Libraries'' by the new section ``Supported Systems''.
+\end{itemize}
+
+\section*{E-ACSL Chlorine-20180501}
+
\begin{itemize}
\item New section \textbf{Additional Verifications}.
-\item Update each section with respect to the changes introduced since \eacsl
+\item Update every section with respect to the changes introduced since \eacsl
Sulfur-20180101.
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 03e8b405449d396dd313d2e5391b52c11f62cc66..1f263c145d11bfd25907b8fb67e7b1b62498321e 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -14,22 +14,29 @@ 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 the \rte plug-in~\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
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index cb007c17c1462a65e53043a7d2d210be6dc61fae..24a3aced3bac7aac92df0a1a8064b8dd5ac123dc 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -12,6 +12,31 @@ some cases, but are tedious to lift. Please contact us if you are interested in
lifting these limitations\footnote{Read \url{http://frama-c.com/support.html}
for additional details.}.
+\section{Supported Systems}
+
+\begin{important}
+The only well-supported system is a Linux distribution on a 64-bit architecture.
+\end{important}
+
+\subsection{Operating Systems}
+
+Non-Linux systems are almost not yet experimented. It might work but there are
+most probably issues, in particular if using a non-standard
+libc\index{Libc}. For instance, there are known bugs under Mac OS
+X\index{Mac OS X}\footnote{See for instance at
+ \url{https://bts.frama-c.com/view.php?id=2369}}.
+
+\subsection{Architectures and Runtime Library}
+
+The segment-based memory model (used by default for monitoring memory properties
+such as \lstinline|\valid|) assumes little-endian architecture and has very
+limited support for 32-bit architectures. When using a 32-bit machine or
+big-endians, we recomend using the bittree-based memory model instead.
+
+\begin{important}
+The runtime library is also \emph{not} thread-safe.
+\end{important}
+
\section{Uninitialized Values}
\index{Uninitialized value}
@@ -130,7 +155,7 @@ A violation of such an annotation $a$ is undetected. There is no workaround yet.
Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
undefined functions. There is also no workaround yet.
-\section{Recursive Function}
+\section{Recursive Functions}
\index{Function!Recursive}
Programs containing recursive functions have the same limitations as the ones
@@ -177,11 +202,3 @@ POSIX-compliant memory management functions
listed above. Monitoring of programs that allocate memory using non-standard or
obsolete functions (e.g., \T{valloc}, \T{memalign}, \T{pvalloc}) may not work
correctly.
-
-\section{Limitations of E-ACSL Monitoring Libraries}
-\index{Function!Libraries}
-
-\eacsl monitoring library implementing segment-based memory model is fairly
-recent and presently has very limited support for 32-bit architectures. When
-using a 32-bit machine we recommend using the bittree-based memory model
-instead.
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index c53111f88fefa4a1c87078b68ae0bda899b939a8..f0e91c4d3dac8ae1e9d0cccfd3b2c92e6f57be42 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -5,19 +5,19 @@
\usepackage{comment}
\newcommand{\framac}{\textsc{Frama-C}\xspace}
-\newcommand{\acsl}{\textsc{ACSL}\xspace}
+\newcommand{\acsl}{\textsc{ACSL}\index{ACSL}\xspace}
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
\newcommand{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
-\newcommand{\rte}{\textsc{RTE}\xspace}
+\newcommand{\rte}{\textsc{RTE}\index{RTE}\xspace}
\newcommand{\C}{\textsc{C}\xspace}
-\newcommand{\jml}{\textsc{JML}\xspace}
-\newcommand{\Eva}{\textsc{Eva}\xspace}
-\newcommand{\variadic}{\textsc{Variadic}\xspace}
-\newcommand{\wpplugin}{\textsc{Wp}\xspace}
-\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
+\newcommand{\jml}{\textsc{JML}\index{JML}\xspace}
+\newcommand{\Eva}{\textsc{Eva}\index{Eva}\xspace}
+\newcommand{\variadic}{\textsc{Variadic}\index{Variadic}\xspace}
+\newcommand{\wpplugin}{\textsc{Wp}\index{WP}\xspace}
+\newcommand{\pathcrawler}{\textsc{PathCrawler}\index{PathCrawler}\xspace}
\newcommand{\gcc}{\textsc{Gcc}\xspace}
-\newcommand{\gmp}{\textsc{GMP}\xspace}
-\newcommand{\dlmalloc}{\textsc{dlmalloc}\xspace}
+\newcommand{\gmp}{\textsc{GMP}\index{GMP}\xspace}
+\newcommand{\dlmalloc}{\textsc{dlmalloc}\index{dlmalloc}\xspace}
\newcommand{\nodiff}{\emph{No difference with \acsl.}}
\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 222ee31e56c7dd2f5f791bc16e0951d58ae1fbae..646e5e344630f84d2484a279cd4f5fd0691c0f42 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -398,7 +398,7 @@ It might be particularly useful in one of the following contexts:
verifying them (for instance, only checking undefine behaviors matters).
\end{itemize}
-\begin{important} \index{eacslgcc}
+\begin{important}
Notably, \eacslgcc disables \framac libc by default. This is because most of
its functions are annotated with \eacsl contracts and generating code for
these contracts results in additional runtime overheads. To enforce default
@@ -552,6 +552,12 @@ potential memory-related annotations even when it is not required. This
feature can be enabled using the \shortopt{M} switch of \eacslgcc or
\shortopt{e-acsl-full-mmodel} option of the \eacsl plug-in.
+\begin{important}
+The above-mentioned static analysis is probably the less robust part of \eacsl
+for the time being. When handling a large piece of code, it might be necessary
+to deactivate it and systematically instrument the code as explained above.
+\end{important}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% \subsection{Debug Libraries}
%% \label{sec:runtime-debug}
@@ -888,8 +894,15 @@ library in order to generate the \framac internal representation of the \C
program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
even if the \eacsl plug-in keeps the maximum amount of information, the results
of already executed analyzers (such as validity status of annotations) are not
-known in this new project. If you want to keep them, you have to set the option
-\shortopt{e-acsl-prepare} when the first analysis is asked for.
+known in this new project.
+
+\begin{important}
+If you want to keep results of former analysis, you have to set the option
+\shortopt{e-acsl-prepare} when the first analysis is asked for. The standard
+example is running \eacsl after \Eva\index{Eva}: in such a case,
+\shortopt{e-acsl-prepare} must be provided together with the \Eva's
+\shortopt{val} option.
+\end{important}
In this context, the \eacsl plug-in does not generate code for annotations
proven valid by another plug-in, except if you explicitly set the option