diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 261adb19591b84eb97cab54d93b8ed32b3b177c5..eff020511a25f23c3a74ef737c2acf792f6182e6 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -1,8 +1,13 @@
MAIN=main
+
+C_CODE=first.i
+
DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
introduction.tex \
provides.tex \
- limitations.tex
+ limitations.tex \
+ $(addprefix examples/, $(C_CODE))
+
default: main.pdf
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 163658f1bcc6ceab054b880cafa4fd3ce1b83580..e5e2195db58a135d2561bcee6b1700c18761511a 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -110,3 +110,15 @@
year = 2012,
month = oct,
}
+
+@article{runtime-assertion-checking,
+ author = {Lori A. Clarke and
+ David S. Rosenblum},
+ title = {A historical perspective on runtime assertion checking in
+ software development},
+ journal = {ACM SIGSOFT Software Engineering Notes},
+ volume = {31},
+ number = {3},
+ year = {2006},
+ pages = {25-37},
+}
diff --git a/src/plugins/e-acsl/doc/userman/examples/first.i b/src/plugins/e-acsl/doc/userman/examples/first.i
new file mode 100644
index 0000000000000000000000000000000000000000..2d0850e1527d97a550283b54e5f1fed45bfc8568
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/first.i
@@ -0,0 +1,6 @@
+int main(void) {
+ int x = 0;
+ /*@ assert x == 0; */
+ /*@ assert x == 1; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 875ce86c4dcaab210ebec636e789d28035aebdac..36ffa716716b1e602cebb33f9d54a04ddcc97115 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -7,8 +7,26 @@ an annotated C code into a \C code which fails at runtime if an annotation is
violated. If no annotation is violated, the behavior of the new program is
exactly the same than the one of the original program.
+Such a translation brings several benefits. First it allows the user to monitor
+a \C code, in particular to perform what is usually called runtime assertion
+checking~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
+ annotation checking'' would be a better more-general expression.}. That is the
+primary goal of \eacsl. Second it allows to combine \framac and its existing
+analyzers, with other analyzer tools for \C, even those who do not 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 runtime
+assertions that cannot be verified statically and to establish a link between
+monitoring tools and static analysis tools like \valueplugin~\cite{value} or
+\wpplugin~\cite{wp}.
+
Annotations must be written in the \eacsl specification
language~\cite{eacsl,sac13} which is a subset of \acsl. This plug-in is still in
a preliminary state: some parts of E-ACSL are not yet supported. Which \eacsl
annotations are currently handled by the \eacsl plug-in is documented in a
separated document~\cite{eacsl-implem}.
+
+This manual does \emph{\textbf{not}} explain how to install the plug-in. Please
+have a look at file \texttt{INSTALL} of the \eacsl tarball for this
+purpose.\index{Installation}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 6364cd48d8bdca3ed259ed4f9db266a83cd56bcf..11a17baf6c88d4b1597d87632f36f9986df0e220 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -6,4 +6,5 @@
\item recursive functions
\item function pointers
\item complex control flow graph
+\item read KNOWN\_BUGS
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index 51719d3d384b090aface34a61becfd4faa963e13..7acb59e67da4048403fb3c336012e5022955a35b 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -9,6 +9,8 @@
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
\newcommand{\C}{\textsc{C}\xspace}
\newcommand{\jml}{\textsc{JML}\xspace}
+\newcommand{\valueplugin}{\textsc{Value}\xspace}
+\newcommand{\wpplugin}{\textsc{Wp}\xspace}
\newcommand{\nodiff}{\emph{No difference with \acsl.}}
\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
@@ -248,3 +250,24 @@
% for texttt
\newcommand{\bs}{\ensuremath{\backslash}}
+
+% Index
+
+\newcommand{\optionidx}[2]{\index{#2@\texttt{#1#2}}}
+\newcommand{\codeidx}[1]{\index{#1@\texttt{#1}}}
+\newcommand{\scodeidx}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}}}
+\newcommand{\sscodeidx}[3]{%
+ \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}}}
+\newcommand{\bfit}[1]{\textbf{\textit{\hyperpage{#1}}}}
+\newcommand{\optionidxdef}[2]{\index{#2@\texttt{#1#2}|bfit}}
+\newcommand{\codeidxdef}[1]{\index{#1@\texttt{#1}|bfit}}
+\newcommand{\scodeidxdef}[2]{\index{#1@\texttt{#1}!#2@\texttt{#2}|bfit}}
+\newcommand{\sscodeidxdef}[3]{%
+ \index{#1@\texttt{#1}!#2@\texttt{#2}!#3@\texttt{#3}|bfit}}
+
+\newcommand{\pragmadef}[1]{\texttt{#1}\index{Pragma!#1@\texttt{#1}}}
+\newcommand{\optiondef}[2]{\texttt{#1#2}\optionidxdef{#1}{#2}}
+\newcommand{\textttdef}[1]{\texttt{#1}\codeidxdef{#1}}
+
+\newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
+\newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index 2af7723511c8e67f4814f6b81bdfb6c1f9812a8a..a16788b2dcc5997af7b36390343f98de4b6d35dd 100644
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 3edf8c1769b2d2b6d78a8bc2d310e01c8f0e08e6..b9b2dccfd6f8e45e350a78fdce6e9d1c886bcfc3 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -76,10 +76,10 @@ future.
%% \addcontentsline{toc}{chapter}{\listfigurename}
%% \listoffigures
-%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% \cleardoublepage
-%% \addcontentsline{toc}{chapter}{\indexname}
-%% \printindex
+\cleardoublepage
+\addcontentsline{toc}{chapter}{\indexname}
+\printindex
\end{document}
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 316c878558df180f183a3bae3524281bcb95d461..8f3eb0c39279d55416e0f1f27232194657a0560a 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -1,19 +1,203 @@
\chapter{What the Plug-in Provides}
+This chapter is the core of this manual and describes how to use the
+plug-in. First, Section~\ref{sec:run} shows how to run the plug-in on a trivial
+example and how to execute the generated code with a standard \C compiler to
+detect invalid annotations at runtime. Then, Section~\ref{sec:custom} introduces
+how to customize the plug-in. Next, Section~\ref{sec:exec} provides additional
+details on the execution of the generated code. Section~\ref{sec:rte} explains
+how the plug-in handles potential runtime errors in the generated code, while
+Section~\ref{sec:incomplete} focus on how to deal with incomplete programs,
+\emph{i.e.} in which some functions have no body or in which there are no main
+function. After, Section~\ref{sec:combine} explains how to combine the plug-in
+with other plug-ins of \framac. Finally, Section~\ref{sec:verbose} details the
+verbosing policy of the plug-in.
+
+\section{Simple Example}
+\label{sec:run}
+
+The main option of the plug-in is \optiondef{-}{e-acsl}. Consider the following
+program.
+
+\listingname{first.i}
+\cinput{examples/first.i}
+Running \eacsl on this file is then pretty simple:
+\begin{shell}
+\$ frama-c -e-acsl first.i
+[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+\end{shell}
+
+Even if \texttt{first.i} is already preprocessed, \eacsl first asks the \framac
+kernel to preprocess and link with \texttt{first.i} several files which forms
+the so-called \eacsl library. Its usefulness will be explain later, mainly in
+Section~\ref{sec:exec}.
+
+Then \eacsl takes the annotated \C code as input and
+translates it into a new \framac project named \texttt{e-acsl}\footnote{The
+ notion of \emph{project} is explained in Section 8.1 of the \framac user
+ manual~\cite{userman}.}. By default, the option \optionuse{-}{eacsl} does
+nothing more. It is however possible to have a look at the generated code on the
+\framac GUI. It is also possible through the command line thanks to the kernel
+options \optionuse{-}{then-on} and \optionuse{-}{print}:
+
+\begin{shell}
+\$ frama-c -e-acsl first.i -then-on e-acsl -print
+[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
+[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@
+model __mpz_struct { integer n };
+*/
+/*@ requires predicate != 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(integer i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) == i;
+ */
+int main(void)
+{
+ int __retres;
+ int x;
+ x = 0;
+ /*@ assert x == 0; */
+ e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
+ /*@ assert x == 1; */
+ e_acsl_assert(x == 1,(char *)"Assertion",(char *)"main",(char *)"x == 1",4);
+ __retres = 0;
+ __clean();
+ return __retres;
+}
+\end{shell}
+
+As you can see, the generated code contains additional type declarations,
+constant declarations and global \acsl annotations that are not in the initial
+file \texttt{first.i}. That is a part of the included \eacsl library. You can
+safely ignore it right now. The translated \texttt{main} function of
+\texttt{first.i} is displayed at the end. Two lines have been added. The first
+one is just after the unique \eacsl annotation.
+
+\begin{ccode}
+ /*@ assert x == 0; */
+ e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",3);
+\end{ccode}
+
+It is a function call to \texttt{e\_acsl\_assert}\codeidx{e\_acsl\_assert} from
+the \eacsl library. This call performs the dynamic verification that the
+corresponding assertion is valid. More precisely, it checks that its first
+argument (here \texttt{x == 0} corresponding to the annotation) is not equal to
+0 and fails otherwise. The extra arguments are only used to display nice user
+feedback as shown later in Section~\ref{sec:exec}.
+
+The second additional line is the call to \texttt{\_\_clean}\codeidx{\_\_clean}
+(once again from the \eacsl library) just before the \texttt{return}
+statement. This call is required to clean potential extra allocations done by
+the \eacsl library (actually none in this example).
+
+By using the option \optionuse{-}{ocode} of \framac, we can redirect the
+generate code into a \C file as follows.
+
+\begin{shell}
+\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
+\end{shell}
+
+\begin{shell}
+\$ gcc -o monitored_first `frama-c -print-share-path`/e-acsl/e_acsl.c
+monitored_first.i
+\$ ./monitored_first
+Assertion failed at line 4 of function main.
+The failing predicate is:
+x == 1.
+\end{shell}
+
+\section{Customizing the Plug-in}
+\label{sec:custom}
+
+\begin{itemize}
+\item -e-acsl-project
+\item -e-acsl-check
+\item -eacsl-share
+\end{itemize}
+
+\section{Execution Environment of the Generated Code}
+\label{sec:exec}
+
\begin{itemize}
-\item simple example illustrating project generation and how to handle this
- project to effectively verify annotations at runtime with GCC.
- (-e-acsl-project)
\item takes care of architecture (32, 64 bits)
\item memory model (linking issue)
\item GMP (linking issue)
-\item incomplete program
- \begin{itemize}
- \item function without code
- \item program without main
- \end{itemize}
\item customizing e\_acsl\_assert
-\item combining E-ACSL with others Frama-C analysis
- (e-acsl-prepare and -e-acsl-valid)
-\item verbosing policy
+\end{itemize}
+
+\section{Potential Runtime Errors in the Generated Code}
+\label{sec:rte}
+
+\begin{itemize}
+\item runtime error in annotations
+\end{itemize}
+
+\section{Handling Incomplete Program}
+\label{sec:incomplete}
+
+\begin{itemize}
+\item function without code
+\item program without main
+\end{itemize}
+
+\section{Combining E-ACSL with Others Plug-ins}
+\label{sec:combine}
+
+\begin{itemize}
+\item -e-acsl-valid
+\item -e-acsl-prepare
+\end{itemize}
+
+\section{Verbosing Policy}
+\label{sec:verbose}
+
+\begin{itemize}
+\item level
+\item category
\end{itemize}