diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 93cc5dffbe794cadf1d005b7177f7d206b221bce..4fdbb389caefa29c3005d363b0bf1aeedbf31da9 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-18.0+dev
+18.0 Argon+dev
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 1c3083282ce04858fe93b1c900986aaa3559b82e..84de44a0272f54fdceff9e8954a0889fdc6345c1 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,8 @@
 #   configure	configure
 ###############################################################################
 
+-  E-ACSL       [2019/02/19] New option -e-acsl-functions to monitor only
+	        annotations in a white list of functions.
 -* runtime      [2019/02/04] Fix initialization of the E-ACSL runtime in
 	        presence of multiple calls to its initializer (for
 	        instance, if the main is a recursive function).
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 453391a0fe0df921974e68fc50b9383f5df39536..c881022e84f8d3f6fd6e8680fcdbd9709117b20d 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -4,7 +4,7 @@ C_CODE=$(wildcard examples/*.[ci])
 VERSION_FILE=../../../../../VERSION
 ifeq ("$(wildcard $(VERSION_FILE))", "")
 VERSION_FILE=../../VERSION
-FC_VERSION= Chlorine
+FC_VERSION= 18.0
 else
 #internal mode
 FC_VERSION=$(shell cat $(VERSION_FILE))
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 5ffb0f549cad04b53f697e13ad5677acf392062e..d27c38a94eef3d42550d895f0c771013cecb55d7 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -5,6 +5,12 @@ release. First we list changes of the last release.
 
 \section*{E-ACSL \eacslversion}
 
+\begin{itemize}
+\item New section \textbf{Providing a White List of Functions}.
+\end{itemize}
+
+\section*{E-ACSL 18.0 Argon}
+
 \begin{itemize}
 \item \textbf{Introduction}: Improve a bit and reference new related papers.
 \item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 646e5e344630f84d2484a279cd4f5fd0691c0f42..c356d00ca393cd5f4204848030e68a26497d425f 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -736,17 +736,21 @@ Abort
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>
-\section{Incomplete Programs} % <<<
+\section{Incomplete Verification} % <<<
 \label{sec:incomplete}
 
 Executing a \C program requires to have a complete application. However, the
 \eacsl plug-in does not necessarily require to have it to generate the
 instrumented code. It is still possible to instrument a partial program with no
-entry point or in which some functions remain undefined.
+entry point (Section~\ref{sec:no-main}) or in which some functions remain
+undefined (Section~\ref{sec:no-code}).
+
+It is also possible to partially instrument an application in order to reduce
+the runtime overhead.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{Programs without Main}
+\subsection{Programs with no Main Function}
 \label{sec:no-main}
 \index{Program!Without main}
 
@@ -786,7 +790,7 @@ x = 65536
 \end{shell}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\
+
 \subsection{Undefined Functions}
 \label{sec:no-code}
 \index{Function!Undefined}
@@ -836,6 +840,19 @@ The execution of the corresponding binary fails at runtime: actually, our
 implementation of the function \texttt{my\_pow} overflows in case of large
 exponentiations.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Providing a White List of Functions}
+\label{sec:white-list}
+\index{Function!White List}
+
+By default, the E-ACSL plug-in generates code for checking at runtime all the
+annotations of the analyzed files. Yet, it is possible to handle only
+annotations of a given set of functions through the option
+\shortopt{e-acsl-functions}. This way, no runtime check is generated for
+annotations of all the other functions. It allows the user to focus on a
+particular part of the code, while reducing the global runtime overhead.
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>