doc + changelog for -e-acsl-functions

src/plugins/e-acsl/VERSION

-18.0+dev
+18.0 Argon+dev

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).

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))

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

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.
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>