[E-ACSL] manual still on the good way

src/plugins/e-acsl/doc/userman/examples/pointer.c

+#include "stdlib.h"
+
+extern void *malloc(size_t);
+extern void free(void*);
+
+int main(void) {
+  int *x;
+  x = (int*)malloc(sizeof(int));
+  *x = 1;
+  /*@ assert *x == 1; */
+  free(x);
+  /*@ assert freed: *x == 1; */
+  return 0;
+}

src/plugins/e-acsl/doc/userman/examples/valid.c

+#include "stdlib.h"
+
+extern void *malloc(size_t);
+extern void free(void*);
+
+int main(void) {
+  int *x;
+  x = (int*)malloc(sizeof(int));
+  /*@ assert \valid(x); */
+  free(x);
+  /*@ assert freed: \valid(x); */
+  return 0;
+}

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

@@ -12,12 +12,18 @@ with other plug-ins of \framac. Finally, Section~\ref{sec:custom} introduces how
 to customize the plug-in, while Section~\ref{sec:verbose} details the verbosing
 policy of the plug-in.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section{Simple Example}
 \label{sec:run}
 
 This Section is a mini-tutorial which explains from scratch how to detect at
 runtime that an \eacsl annotation is violated thanks to the use of the plug-in.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsection{Running \eacsl}
 
 Consider the following simple program in which the first assertion is valid
@@ -138,6 +144,8 @@ corresponding to the annotations) 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}.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsection{Executing the generated code}
 
 By using the option \optionuse{-}{ocode} of \framac, we can redirect the
@@ -182,6 +190,10 @@ the invalid \eacsl annotation has been violated. There is no output for the
 valid \eacsl annotation. So, thanks to the plug-in, we detect that one of the
 assertion in the initial program was wrong.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section{Execution Environment of the Generated Code}
 \label{sec:exec}
 
@@ -190,7 +202,10 @@ one supposed to be by \framac. You must take care of that when running the
 plug-in and when compiling the generated code with \gcc. Also, the plug-in
 offers you few possibilities of customization.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsection{Runtime Errors in Annotations}
+\label{sec:runtime-error}
 \index{Runtime Error}
 
 The major difference between \acsl~\cite{acsl} and \eacsl~\cite{eacsl}
@@ -234,6 +249,8 @@ The failing predicate is:
 division_by_zero: y != 0.
 \end{shell}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsection{Architecture}
 
 In many cases, the execution of a \C program depends on the underlying machine
@@ -275,6 +292,14 @@ sizeof(long) == 8.
 There is no assertion failure if you add the option \texttt{-machdep x86\_64}
 when calling \framac.
 
+\begin{shell}
+\$ frama-c -machdep x86_64 -pp-annot -e-acsl archi.c \
+           -then-on e-acsl -print -ocode monitored_archi.i
+\end{shell}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsection{\gmp}
 \index{GMP}
 
@@ -282,27 +307,140 @@ when calling \framac.
 integers. Of course such integers do 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 \C integral type instead of \gmp~\cite{sac13}, it may generate
-such integers from time to time. In such cases, the generated code must be
-linked against \gmp to be executed.
+use standard \C integral type instead of \gmp~\cite{sac13}, it may generate such
+integers from time to time. In such cases, the generated code must be linked
+against \gmp to be executed.
 
 Consider for instance the following program.
 
-\listingname{gmp}
+\listingname{gmp.i}
 \cinput{examples/gmp.i}
 
-\subsection{Memory Model}
-\cite{rv13}
+Even on a 64 bits machine, it is not possible to compute the assertion with a
+standard \C type. In this case, the plug-in generates \gmp code.
+
+We can however generate an instrumented code as usual through the
+following command lines:
+
+\begin{shell}
+\$ frama-c -e-acsl gmp.i -then-on e-acsl -print -ocode monitored_gmp.i
+\end{shell}
+
+To compile it however, we need to have \gmp installed and to add the option
+\optionuse{-}{lgmp} to \gcc as follows:
+
+\begin{shell}
+\$ gcc -o gmp `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_gmp.i -lgmp
+\end{shell}
+
+We can now execute it as usual.
+\begin{shell}
+\$ ./gmp
+\end{shell}
+
+Since the assertion is valid, there is no output in this case.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Memory-related Annotations}
+
+The \eacsl plug-in translated memory-related annotations like
+\lstinline|\valid|. When using such an annotation, the generated code must be
+linked against a dedicated library installed with the plug-in to be
+executed. This library includes two \C files which are installed in the \eacsl'
+share directory:
+\begin{itemize}
+\item \texttt{memory\_model/e\_acsl\_bittree.c}; and
+\item \texttt{memory\_model/e\_acsl\_mmodel.c}.
+\end{itemize}
+
+Consider for instance the following program.
+
+\listingname{valid.c}
+\cinput{examples/valid.c}
+
+Assuming that we want to execute the generated code on a x86 64 bits machine,
+the generation of the instrumented code by using the plug-in requires the use of
+the option \optionuse{-}{machdep} since the code uses \texttt{sizeof}. However,
+nothing more is required here.
+
+\begin{shell}
+\$ frama-c -machdep x86_64 -e-acsl valid.c -then-on e-acsl -print -ocode monitored_valid.i
+\end{shell}
+
+However, since the original code uses \lstinline|\valid|, the executable binary
+must be generated from \texttt{monitored\_valid.i} as follows:
+
+\begin{shell}
+\$ DIR=`frama-c -print-share-path`/e-acsl
+\$ MDIR=\$DIR/memory_model
+\$ gcc -o valid \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \$MDIR/e_acsl_mmodel.c monitored_valid.i
+\end{shell}
+
+Now we can execute the generate binary which fails at runtime since the second
+assertion is violated.
+\begin{shell}
+\$ ./valid
+Assertion failed at line 11 in function main.
+The failing predicate is:
+freed: \valid(x).
+\end{shell}
+
+Like for integers, we do our best to use the dedicated library only when
+required~\cite{rv13}. So, if your program does not contain memory-related
+annotations, the generated one does not require to be linked against the
+dedicated memory library.
+
+Note however that if your program has annotations with pointer dereferencing
+(for instance), then the generated code \emph{does} require to be linked against
+the dedicated library at compile time. Why? Because pointer dereferencing may
+lead to runtime errors, so \eacsl inserts runtime checks to prevent them
+according to Section~\ref{sec:runtime-error} as shown by the following example.
+
+\listingname{pointer.c}
+\cinput{examples/pointer.c}
+
+\begin{shell}
+\$ frama-c -machdep x86_64 -e-acsl pointer.c -then-on e-acsl -print -ocode
+monitored_pointer.i
+\$ DIR=`frama-c -print-share-path`/e-acsl
+\$ MDIR=\$DIR/memory_model
+\$ gcc -o pointer \$DIR/e_acsl.c \$MDIR/e_acsl_bittree.c \$MDIR/e_acsl_mmodel.c\
+       monitored_pointer.i
+\$ ./pointer
+RTE failed at line 0 in function main.
+The failing predicate is:
+mem_access: \valid_read(x).
+\end{shell}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Customizing the Behavior of the Executed Code}
 
+\todo{Modifying e\_acsl\_assert}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section{Handling Incomplete Program}
 \label{sec:incomplete}
 
-\begin{itemize}
-\item function without code
-\item program without main
-\end{itemize}
+Executing a \C program requires to have a complete application. However, the
+\eacsl plug-in does not necessarily require to get it to generate the
+instrumented code.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Program without Main}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Function without Code}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \section{Combining E-ACSL with Others Plug-ins}
 \label{sec:combine}
@@ -312,6 +450,16 @@ Consider for instance the following program.
 \item -e-acsl-prepare
 \end{itemize}
 
+annotations are kept in order to analyze the generated code
+
+possible to run rte first
+
+combination with value and wp
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section{Customizing the Plug-in}
 \label{sec:custom}
 
@@ -321,6 +469,10 @@ Consider for instance the following program.
 \item -eacsl-share
 \end{itemize}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section{Verbosing Policy}
 \label{sec:verbose}