[E-ACSL] userman is on the way

src/plugins/e-acsl/doc/userman/Makefile

 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
 

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},
+}

src/plugins/e-acsl/doc/userman/examples/first.i

+int main(void) {
+  int x = 0;
+  /*@ assert x == 0; */
+  /*@ assert x == 1; */
+  return 0;
+}

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}

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}

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

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}

src/plugins/e-acsl/doc/userman/provides.tex

 \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}