diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 27d9be4791f802dbe9eebcb8cd3ed69c8cbe2139..63e742e131e03df9a6f38531c3b56c3ad2b18246 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -59,6 +59,25 @@
url = {publis/hdr.pdf}
}
+@inproceedings{kosmatov20rv,
+ author = {Kosmatov, Nikolai and Maurica, Fonenantsoa and Signoles, Julien},
+ title = {{Efficient Runtime Assertion Checking for Properties over
+ Mathematical Numbers}},
+ booktitle = {International Conference on Runtime Verification (RV)},
+ year = 2020,
+ month = oct,
+}
+
+@inproceedings{ly18hilt,
+ author = {Dara Ly and Nikolai Kosmatov and Fr\'ed\'eric Loulergue
+ and Julien Signoles},
+ title = {Soundness of a Dataflow Analysis for Memory Monitoring},
+ booktitle = {Workshop on Languages and Tools for Ensuring Cyber-Resilience in
+Critical Software-Intensive Systems (HILT)},
+ year = 2018,
+ month = nov,
+}
+
@inproceedings{rvcubes17tool,
author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index c69ab6038c6d344e0bbf612f2d171f4c96482979..034766eaca3e2ae51a6764834055cbb5dc55777e 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -5,6 +5,14 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslpluginversion}
+\begin{itemize}
+\item \textbf{Simple Example}: Remove option \texttt{-e-acsl-check}
+\item \textbf{Combining E-ACSL with Other PLug-ins}: \texttt{-e-acsl-prepare} is
+ no more necessary.
+\end{itemize}
+
+\section*{E-ACSL 19.0 Potassium}
+
\begin{itemize}
\item \textbf{Runtime Monitor Behavior}: Document global variable
\texttt{\_\_e\_acsl\_sound\_verdict} usable in \texttt{\_\_e\_acsl\_assert}.
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index ec0d86ba6c26d28e71a791c5268787dcd87b2908..c42ab93808d1fb2fbfb644ce3e4293bbeb443485 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -152,9 +152,6 @@ $f$ such that:
\end{itemize}
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.
-
\subsection{Incomplete Types}
\index{Type!Incomplete}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 172397d5d4013c43680dd271eb5b4d7420805874..f2f73c8229cab00bfd68472c81be15710c4f45ae 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -50,8 +50,9 @@ evolve in the future.
\section*{Acknowledgements}
We gratefully thank the people who contributed to this document:
-Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola\"i Kosmatov,
-Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot.
+Basile Desloges, Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner,
+Nikola\"i Kosmatov, Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and
+Guillaume Petiot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 18df5fe9d39c61acac7b65e4a931299f9e7f7c71..accd222ac1c299c54589bc2c69647b8855ab3ec6 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -416,7 +416,7 @@ script.
mathematical integers which does not fit in any integral \C type. To circumvent
this issue, \eacsl uses the \gmp library\footnote{\url{http://gmplib.org}}.
Thus, even if \eacsl does its best to use standard integral types instead of
-\gmp~\cite{sac13,jfla15}, it may generate such integers from time to time. It is
+\gmp~\cite{kosmatov20rv}, it may generate such integers from time to time. It is
notably the case if your program contains \lstinline|long long|, either signed
or unsigned.
@@ -544,8 +544,8 @@ model~\cite{pldi16}.
\subsubsection{Maximized Memory Tracking}
By default \eacsl uses static analysis to reduce instrumentation and therefore
-runtime and memory overheads~\cite{scp16}. With respect to memory tracking this
-means that
+runtime and memory overheads~\cite{ly18hilt}. With respect to memory tracking
+this means that
\eacsl may omit recording memory blocks irrelevant for runtime analysis. It
is, however, still possible to systematically instrument the code for handling
potential memory-related annotations even when it is not required. This
@@ -980,22 +980,6 @@ The present implementation of \eacslgcc does not fully support combining \eacsl
with other \framac plug-ins. However it is still possible to instrument programs
with \eacsl directly and use \eacslgcc to compile the generated code.
-If you run the \eacsl plug-in after another one, it first generates
-a new temporary project in which it links the analyzed program against its own
-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.
-
-\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
\shortopt{e-acsl-valid}. For instance, \Eva~\cite{eva} is able to
@@ -1003,21 +987,14 @@ prove that there is no potential overflow in the previous program, so the \eacsl
plug-in does not generate additional code for checking them if you run the
following command.
\begin{shell}
-\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+\$ frama-c -rte combine.i -then -val -then -e-acsl \
-then-last -print -ocode monitored_combine.i
\end{shell}
-The additional code will be generated with one of the two following commands.
+The additional code will be generated with the two following command.
\begin{shell}
-\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
- -e-acsl-valid -then-last -print -ocode monitored_combine.i
\$ frama-c -rte combine.i -then -val -then -e-acsl \
- -then-last -print -ocode monitored_combine.i
+ -e-acsl-valid -then-last -print -ocode monitored_combine.i
\end{shell}
-In the first case, that is because it is explicitly required by the option
-\shortopt{e-acsl-valid} while, in the second case, that is because the option
-\shortopt{e-acsl-prepare} is not provided on the command line which results in
-the fact that the result of the value analysis are unknown when the \eacsl
-plug-in is running.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1044,20 +1021,6 @@ check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
[e-acsl] translation done in project "foobar".
\end{shell}
-Further, the \eacsl plug-in option \shortopt{e-acsl-check} does not generate a
-new project but verifies that each annotation is translatable. Then it produces
-a summary as shown in the following example (left or right shifts in annotations
-are not yet supported by the \eacsl plug-in~\cite{eacsl-implem}).
-
-\begin{shell}
-\$ frama-c -e-acsl-check check.i
-<skip preprocessing commands>
-check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
- Ignoring annotation.
-[e-acsl] 0 annotation was ignored, being untypable.
-[e-acsl] 1 annotation was ignored, being unsupported.
-\end{shell}
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>