diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 945b09e32f12951089902bcfec0c3d192ad7bcc7..386e5b6343c61374c28348b0c5585bcc7da68126 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,7 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
--  E-ACSL       [2016/02/03] Added scripts/testrun.sh - a convenience wrapper
+o  E-ACSL       [2016/02/03] Added scripts/testrun.sh - a convenience wrapper
 	        around e-acsl-gcc.sh for use with testing.
 -* E-ACSL       [2016/01/15] Fix installation with custom --prefix.
 -* E-ACSL       [2016/01/05] Fix bug in the memory model that caused the
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 008cf267af995537f7ece3fc7f26bfdcea23d019..f4d2455de54c1c2c299e42c41a2103b5f88e0b39 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/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 25aafc00b0e30815481e645605c075a3e4ac397a..33d00dbf8c6f8a208100ba2d951548bc8621411c 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -8,6 +8,7 @@ DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
 	provides.tex \
 	limitations.tex \
 	changes.tex \
+	eacslgcc.tex \
 	$(C_CODE) \
 	$(VERSION_FILE)
 
@@ -20,7 +21,7 @@ FC_VERSION= Sodium
 
 EACSL_DIR=../..
 DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
-install: 
+install:
 	cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
 #	cp -f main.pdf \
 	  $(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
diff --git a/src/plugins/e-acsl/doc/userman/eacslgcc.tex b/src/plugins/e-acsl/doc/userman/eacslgcc.tex
new file mode 100644
index 0000000000000000000000000000000000000000..43f8e99a9d6c86f50f0400b74b6a4873d9846237
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/eacslgcc.tex
@@ -0,0 +1,183 @@
+\chapter{Easy Instrumentation with \eacsl}
+
+Due to numerous instrumentation and compile-time options generating monitored
+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.
+
+In this section we describe \eacslgcc and provide several examples of its use.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Basic Use}
+
+\eacslgcc instruments C files provided at input using the \eacsl plug-in, and
+optionally compiles the generated code and the original sources using a \C
+compiler (\gcc by default).
+
+The default behaviour of \eacslgcc is to instrument an annotated C program
+with runtime assertions via a run of \framac.
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -ogen.c foo.c
+\end{shell}
+
+The above command instruments \texttt{foo.c} with runtime assertions and
+outputs the generated code to \texttt{gen.c}. Unless the name of the output
+file is specified via the \texttt{-o} option (i.e., \texttt{-ogen.c} in the
+above example), the generated code is placed to a file named
+\texttt{a.out.frama.c}.
+
+Compilation of the original and the instrumented sources
+is enabled using the \texttt{-c} option.  For instance, the command
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -ogen.c foo.c
+\end{shell}
+
+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.
+
+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 generated from the
+\eacsl-instrumented code is suffixed \texttt{.e-acsl}.
+
+For example, command
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -ogen.c -Ogen foo.c
+\end{shell}
+names 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 the instrumentation step and
+compile a given program as if it were already instrumented by the \eacsl
+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}
+ \$ e-acsl-gcc.sh -C -Ogen gen.c
+\end{shell}
+
+In the above example the run of \eacslgcc produces a single executable named
+\texttt{gen.e-acsl}. This is because \texttt{gen.c} is considered to be
+instrumented code and thus no original program is provided.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Documentation}
+
+A list of \eacslgcc options can be retrieved using the following command:
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -h
+ Usage: e-acsl-gcc.sh [options] files
+ Options:
+   -h         show this help page
+   -c         compile instrumented code
+   -l         pass additional options to the linker
+   -e         pass additional options to the pre-preprocessor
+   -E         pass additional arguments to the Frama-C pre-processor
+   -p         output the generated code with rich formatting to STDOUT
+   -o <file>  output the generated code to <file> [a.out.frama.c]
+   -O <file>  output the generated executables to <file> [a.out, a.out.e-acsl]
+   -M         maximize memory-related instrumentation
+   -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 executable without debug features
+   -I <file>  specify Frama-C executable [frama-c]
+   -G <file>  specify GCC executable [gcc]
+\end{shell}
+
+Note that the \texttt{-h} option lists only the most basic options.
+For full up-to-date documentation of \eacslgcc see its man page:
+
+\begin{shell}
+    \$ man e-acsl-gcc.sh
+\end{shell}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Customising \framac and \gcc Invocations}
+
+Runs of \framac and \gcc issued by \eacslgcc can be customized by using
+additional flags.
+
+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
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c
+\end{shell}
+
+yields an instrumented program \texttt{a.out.frama.c} where ACSL formulas
+are output using the UTF-8 character set. Further, during the compilation of
+\texttt{a.out.frama.c} \gcc adds directories \texttt{/bar} and
+\texttt{/baz} to the list of directories to be searched for header files.
+
+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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Verbosity Levels and Output Redirection}
+
+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 plug-ins but suppress the verbosity of
+the \framac kernel while instrumenting \texttt{foo.c} one can use the following
+command:
+
+\begin{shell}
+ \$ e-acsl-gcc.sh -v5 -F"-kernel-verbose 0" foo.c
+\end{shell}
+
+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 file using the
+\texttt{-s} option.  For example, the following command redirects 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
+\end{shell}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Executables}
+
+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 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 changed similarly using the \texttt{-G}
+option.
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index c5c52f75339852fb785f00a2d0f75318e5913e1d..61572c7cba1c1e522b54dadcfd74599feaef92fd 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -7,6 +7,7 @@
 \newcommand{\framac}{\textsc{Frama-C}\xspace}
 \newcommand{\acsl}{\textsc{ACSL}\xspace}
 \newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
+\newcommand{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
 \newcommand{\rte}{\textsc{RTE}\xspace}
 \newcommand{\C}{\textsc{C}\xspace}
 \newcommand{\jml}{\textsc{JML}\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index 412182a639a3dc77a1260f972ea31eb47f29297a..4d713e7d3e24c0f3770b4bcf2627a4afa77345bb 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -19,7 +19,7 @@
 \vfill
 \title{\eacsl Plug-in}{Release \eacslversion compatible 
   with \framac \fcversion}
-\author{Julien Signoles}
+\author{Julien Signoles and Kostyantyn Vorobyov}
 \begin{tabular}{l}
 CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
 \end{tabular}
@@ -56,6 +56,7 @@ Guillaume Petiot.
 
 \include{introduction}
 \include{provides}
+\include{eacslgcc}
 \include{limitations}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 47981cbfc6d7bcc3f5aa4ee7bddc33308bf70f7e..da6ca9a13c39a581fdffa34883d680953313533d 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
@@ -773,3 +773,5 @@ typing & minimization of the instrumentation for integers
 \hline
 \end{tabular}
 \end{center}
+
+
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index f1b8bee53f38e1b9f61c94befbe33df772a028a7..89a2589d746259709b9375dde1a476dad5069223 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -92,7 +92,7 @@ Options:
   -p         output the generated code with rich formatting to STDOUT
   -o <file>  output the generated code to <file> [a.out.frama.c]
   -O <file>  output the generated executables to <file> [a.out, a.out.e-acsl]
-  -M         maximise memory-related instrumentation
+  -M         maximize memory-related instrumentation
   -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>
@@ -307,7 +307,6 @@ check_tool "$OPTION_CC"
 
 # Frama-C and related flags
 FRAMAC="$OPTION_FRAMAC"
-FRAMAC_FLAGS=""
 FRAMAC_SHARE="`$FRAMAC -print-share-path`"
 FRAMAC_CPP_EXTRA="
   $OPTION_FRAMAC_CPP_EXTRA