diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf
index 7a0cc6906e73eed064b795bbf182b7c861ce50d9..c6cb31bbdb707182f389100e531595eec6277a48 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index f48756c39dac6083ad57a1d08f621a19139b59dc..cf27296c58844e5bf79ea5d45469185ffa2daec5 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -101,9 +101,9 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
 
 /*@
 axiomatic dynamic_allocation {
-  predicate is_allocable{L}(size_t n) 
+  predicate is_allocable{L}(size_t n)
     reads __fc_heap_status;
-  
+
   }
  */
 /*@ ghost extern int __e_acsl_init; */
@@ -135,7 +135,7 @@ constant declarations and global \acsl annotations that are not in the initial
 file \texttt{first.i}. They are part of the included \eacsl monitoring
 library. You can safely ignore it right now. The translated \texttt{main}
 function of \texttt{first.i} is displayed at the end. After each \eacsl
-annotation, a line has been added. 
+annotation, a line has been added.
 
 \begin{ccode}
   /*@ assert x == 0; */
@@ -519,9 +519,9 @@ restrictions.
 
 The \eacsl plug-in may work even if there is no \texttt{main} function.
 Consider for instance the following annotated program without such a
-\texttt{main}.  
+\texttt{main}.
 
-\listingname{no\_main.i} 
+\listingname{no\_main.i}
 \cinput{examples/no_main.i}
 
 The instrumented code is generated as usual, even though you get an additional
@@ -565,7 +565,7 @@ The \eacsl plug-in may also work if some functions have no implementation.
 Consider for instance the following annotated program for which the
 implementation of the function \texttt{my\_pow} is not provided.
 
-\listingname{no\_code.c} 
+\listingname{no\_code.c}
 \cinput{examples/no_code.c}
 
 The instrumented code is generated as usual, even though you get an additional
@@ -575,7 +575,7 @@ warning.
 [e-acsl] warning: annotating undefined function `my_pow':
                   the generated program may miss memory instrumentation
                   if there are memory-related annotations.
-[kernel] warning: No code nor implicit assigns clause for function my_pow, 
+[kernel] warning: No code nor implicit assigns clause for function my_pow,
 generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 \end{shell}
@@ -647,7 +647,7 @@ even if the \eacsl plug-in keeps the maximum amount of information, the results
 of already executed analyzers (such as validity status of annotations) are not
 known in this new project. If you want to keep them, you have to set the option
 \optiondef{-}{e-acsl-prepare} when the first analysis is asked for.
- 
+
 In this context, the \eacsl plug-in does not generate code for annotations
 proven valid by another plug-in, except if you explicitly set the option
 \optiondef{-}{e-acsl-valid}. For instance, \valueplugin~\cite{value} is able to
@@ -678,7 +678,7 @@ plug-in is running.
 \section{Customization}
 \label{sec:custom}
 
-There are several ways to customize the \eacsl plug-in. 
+There are several ways to customize the \eacsl plug-in.
 
 First, the name of the generated project -- which is \texttt{e-acsl} by
 default -- may be changed by setting the option \optiondef{-}{e-acsl-project}.
@@ -760,7 +760,7 @@ parts of the translation, as detailed below.
 \begin{center}
 \begin{tabular}{|l|l|}
 \hline
-analysis & minimization of the instrumentation for memory-related annotation 
+analysis & minimization of the instrumentation for memory-related annotation
 (section~\ref{sec:memory}) \\
 \hline
 duplication & duplication of functions with contracts
@@ -782,7 +782,7 @@ typing & minimization of the instrumentation for integers
 \label{sec:eacsl-gcc}
 
 Due to numerous instrumentation and compile-time options generating monitored
-executables using the \eacsl plugin can be tedious. To simplify this task we
+executables using the \eacsl plug-in can be tedious. To simplify this task we
 developed \eacslgcc\ -- a convenience wrapper around \framac and \gcc allowing
 to instrument programs with \eacsl and compile the instrumented code using a
 single command and a very few parameters.
@@ -793,7 +793,7 @@ In this section we describe \eacslgcc and provide several examples of its use.
 
 \subsection{Basic Use}
 
-\eacslgcc instruments C files provided at input using the \eacsl plugin, and
+\eacslgcc instruments C files provided at input using the \eacsl plug-in, and
 optionally compiles the generated code and the original sources using the \gcc
 compiler.
 
@@ -819,13 +819,13 @@ is enabled using the \texttt{-c} option.  For instance, the command
 
 instruments the code in \texttt{foo.c}, outputs it to \texttt{gen.c} and
 produces 2 executables: \texttt{a.out} and \texttt{a.out.e-acsl}, where
-\texttt{a.out} is an executable compiled from
-\texttt{foo.c}, while \texttt{a.out.e-acsl} is an executable compiled from
-\texttt{gen.c} generated by \eacsl.
+\texttt{a.out} is an executable compiled from \texttt{foo.c}, while
+\texttt{a.out.e-acsl} is an executable compiled from \texttt{gen.c} generated
+by \eacsl.
 
 Named executables can be created using the \texttt{-O} option.  This is such
 that a value supplied to the \texttt{-O} option is used to name the executable
-generated from the original program and the executable generateted from the
+generated from the original program and the executable generated from the
 \eacsl-instrumented code is suffixed \texttt{.e-acsl}.
 
 For example, command
@@ -835,9 +835,9 @@ For example, command
 will name the executables generated from \texttt{foo.c} and \texttt{gen.c}:
 \texttt{gen} and \texttt{gen.e-acsl} respectively.
 
-The \eacslgcc \texttt{-C} option allows to skip instrumentation step and
+The \eacslgcc \texttt{-C} option allows to skip the instrumentation step and
 compile a given program as if it were already instrumented by the \eacsl
-plugin.  This option is useful if one makes some changes to an already
+plug-in.  This option is useful if one makes changes to an already
 instrumented source file by hand and only wants to recompile it.
 
 \begin{shell}
@@ -870,7 +870,7 @@ A list of \eacslgcc options can be retrieved using the following command:
    -g         always use GMP integers instead of C integral types
    -q         suppress any output except for errors and warnings
    -s <file>  redirect all output to <file>
-   -P         compile executatle without debug features
+   -P         compile executable without debug features
    -I <file>  specify Frama-C executable [frama-c]
    -G <file>  specify GCC executable [gcc]
 \end{shell}
@@ -886,13 +886,12 @@ For full up-to-date documentation of \eacslgcc see its man page:
 
 \subsection{Customising \framac and \gcc Invocations}
 
-Runs of \framac and \gcc issued by \eacslgcc can be customized by
-using additional flags passed the tools' invocations.
+Runs of \framac and \gcc issued by \eacslgcc can be customized by using
+additional flags passed the tools' invocations.
 
 Additional \framac flags can be passed using the \texttt{-F} option, while
 \texttt{-l} and \texttt{-e} options allow for passing additional pre-processor
-and linker flags during \gcc invocations.
-For example, command
+and linker flags during \gcc invocations.  For example, command
 
 \begin{shell}
  \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
@@ -905,8 +904,8 @@ are output using the UTF-8 character set. Further, during the compilation of
 
 It is worth mentioning that \eacslgcc implements several convenience flags for
 setting some of the \framac options. For instance, \texttt{-E} can be used to
-pass additional arguments to the \framac pre-processor and \texttt{-M} maximizes
-memory-related instrumentation.
+pass additional arguments to the \framac pre-processor and \texttt{-M}
+maximizes memory-related instrumentation.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -916,7 +915,7 @@ By default \eacslgcc prints the executed \framac and \gcc commands and pipes
 their output to the terminal. The verbosity of \framac output can be changed
 using \texttt{-v} and \texttt{-d} options used to pass values to
 \texttt{-verbose} and \texttt{-debug} flags of \framac respectively.  For
-instance, to increase the verbosity of plugins but suppress the verbosity of
+instance, to increase the verbosity of plug-ins but suppress the verbosity of
 the \framac kernel while instrumenting \texttt{foo.c} one can use the following
 command:
 
@@ -924,14 +923,14 @@ command:
  \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
 \end{shell}
 
-Verbosity of the output of \eacslgcc script can also be reduced using the
-\texttt{-q} option that suppresses any output except errors or warnings issued
-by \gcc, \framac or \eacslgcc itself.
+Verbosity of the \eacslgcc output can also be reduced using the \texttt{-q}
+option that suppresses any output except errors or warnings issued by \gcc,
+\framac or \eacslgcc itself.
 
-The output of \eacslgcc can also be redirected to a specified log file
-using the \texttt{-s} option.  For example, the following command will redirect
-all output during instrumentation and compillation of \texttt{foo.c} to the
-\texttt{/tmp/log} file.
+The output of \eacslgcc can also be redirected to a specified file using the
+\texttt{-s} option.  For example, the following command will redirect all
+output during instrumentation and compilation of \texttt{foo.c} to the
+file named \texttt{/tmp/log}.
 
 \begin{shell}
  \$ e-acsl-gcc.sh -c -s/tmp/log foo.c
@@ -945,11 +944,11 @@ By default \eacslgcc uses the first \texttt{frama-c} executable found in a
 system's path to instrument input programs. The name of the \framac executable
 can be changed using the \texttt{-I} option. For instance, to instrument a file
 named \texttt{foo.c} using the \texttt{/usr/local/bin/frama-c.byte} executable
-one can issue the following command:
+one can use the following command:
 
 \begin{shell}
  \$ e-acsl-gcc.sh -I/usr/local/bin/frama-c.byte foo.c
 \end{shell}
 
-The name of a \gcc executable can be similarly changed using the \texttt{-G}
-option.
\ No newline at end of file
+The name of a \gcc executable can be changed similarly using the \texttt{-G}
+option.