diff --git a/src/plugins/e-acsl/doc/refman/e-acsl.pdf b/src/plugins/e-acsl/doc/refman/e-acsl.pdf
index b7ed786018125b9cd5296675eac11e155f37c75e..6e477abc5f1a5e33305da7c9ad9fccaa1719f6fb 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index d57089afd1917808596084bf64e63ff694a00051..78dd60f322a6792828df0e5915a3500d9d6062f5 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -223,7 +223,7 @@ Below, the first term is well-defined, while the second one is undefined.
 
 \paragraph{Handling undefinedness in tools}
 
-It is the responsibility of the tools which interprets \eacsl to ensure that an
+It is the responsibility of each tool which interprets \eacsl to ensure that an
 undefined term is never evaluated. For instance, they may exit with a proper
 error message or, if they generate \C code, they may guard each generated
 undefined \C expression in order to be sure that they are always safely used.
diff --git a/src/plugins/e-acsl/doc/userman/examples/archi.c b/src/plugins/e-acsl/doc/userman/examples/archi.c
index 9f2d2ae6a1957f9e0001e7308736e91c02d3eb02..4d4861bb169af87cf9213b16ec17354f3b4f5a51 100644
--- a/src/plugins/e-acsl/doc/userman/examples/archi.c
+++ b/src/plugins/e-acsl/doc/userman/examples/archi.c
@@ -1,4 +1,4 @@
-#define ARCH_BITS 64 /* assume a 64 bits architecture */
+#define ARCH_BITS 64 /* assume a 64-bit architecture */
 
 #if ARCH_BITS == 32
 #define SIZEOF_LONG 4
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 1cebee57deee697d993838fe951079813a0aff26..5427255fb71de682dc4b7cad12e6af7160cd8639 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -2,19 +2,19 @@
 
 \framac~\cite{userman,sefm12} is a modular analysis framework for the C language
 which supports the ACSL specification language~\cite{acsl}. This manual
-documents the \eacsl plug-in of \framac, version \eacslversion. Which \eacsl
-version you are using is indicated by running \texttt{frama-c
+documents the \eacsl plug-in of \framac, version \eacslversion. The \eacsl
+version you are using is indicated by the command \texttt{frama-c
   -e-acsl-version}\optionidx{-}{e-acsl-version}. This plug-in automatically
 translates an annotated C program into another program that 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.
+program is exactly the same as 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.}. This is the
 primary goal of \eacsl. Second it allows the combination of \framac and its
-existing analyzers, with other analyzer tools for \C like
+existing analyzers, with other analyzers for \C like
 \pathcrawler~\cite{pathcrawler} that do not natively understand the \acsl
 specification language. Third, the possibility to detect invalid annotations
 during a concrete execution may be very helpful while writing a correct
@@ -26,8 +26,8 @@ monitoring tools and static analysis tools like
 
 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
+a preliminary state: some parts of E-ACSL are not yet supported. \eacsl
+annotations currently handled by the \eacsl plug-in are documented in a
 separated document~\cite{eacsl-implem}.
 
 This manual does \emph{not} explain how to install the plug-in. Please
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index d428ad162ac7fe414b1176d30b3ab7bcd93dc8e6..124d6563bdc06b13277d6e44384ba920d6f7c15e 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -1,15 +1,15 @@
 \chapter{Known Limitations}
 
-The development of the \eacsl plug-in is still ongoing. First, the whole \eacsl
-reference manual~\cite{eacsl} is not yet supported. Which annotations are
+The development of the \eacsl plug-in is still ongoing. First, the \eacsl
+reference manual~\cite{eacsl} is not yet fully supported. Which annotations are
 already translated into \C code and which are not is defined in a separated
-document~\cite{eacsl-implem}. Second, even though we do our best, bugs may
-exist. If you find a new one, please report it on the bug tracking system (see
-Chapter 10 of the \framac User Manual~\cite{userman}). Third, there are some
-additional known limitations, which could be annoying for the user in some
-cases, but are hard to lift. Please contact us if you are interested in lifting
-these limitations\footnote{Read \url{http://frama-c.com/support.html} for
-  additional details.}.
+document~\cite{eacsl-implem}. Second, even though we do our best to avoid them,
+bugs may exist. If you find a new one, please report it on the bug tracking
+system (see Chapter 10 of the \framac User Manual~\cite{userman}). Third, there
+are some additional known limitations, which could be annoying for the user in
+some cases, but are tedious to lift. Please contact us if you are interested in
+lifting these limitations\footnote{Read \url{http://frama-c.com/support.html}
+  for additional details.}.
 
 \section{Uninitialized Values}
 \index{Uninitialized value}
@@ -37,9 +37,9 @@ monitored_uninitialized.i:44:16: warning: 'x' is used uninitialized in this func
 \$ ./monitored_uninitialized
 \end{shell}
 
-This is more a design choice that a limitation: should the \eacsl plug-in
-generate additional instrumentation to prevent such values to be executed, the
-generated code would be much more verbose and much slower.
+This is more a design choice than a limitation: should the \eacsl plug-in
+generate additional instrumentation to prevent such values from being evaluated,
+the generated code would be much more verbose and slower.
 
 If you really want to track such uninitializations in your annotation, you have
 to manually add calls to the \eacsl predicate
@@ -49,7 +49,7 @@ to manually add calls to the \eacsl predicate
 
 Section~\ref{sec:incomplete} explains how the \eacsl plug-in is able to handle
 incomplete programs, which are either programs without main, or programs
-containing functions without bodies.
+containing undefined functions (\emph{i.e.} functions without body).
 
 However, if such programs contain memory-related annotations, the generated code
 may be incorrect. That is made explicit by a warning displayed when the \eacsl
@@ -60,9 +60,10 @@ plug-in is running (see examples of Sections~\ref{sec:no-main} and
 \index{Program!Without main}
 \label{sec:limits:no-main}
 
-The generated program is incorrect for every program without main containing a
-memory-related annotations, except if the option
-\optionuse{-}{e-acsl-full-mmodel} is provided.
+The instrumentation in the generated program is partial for every program
+without main containing a memory-related annotations, except if the option
+\optionuse{-}{e-acsl-full-mmodel} is provided. In that case, violations of such
+annotations are undetected.
 
 Consider the following example.
 
@@ -106,42 +107,42 @@ The failing predicate is:
 freed: \valid(x).
 \end{shell}
 
-\subsection{Functions without Code}
+\subsection{Undefined Functions}
 \label{sec:limits:no-code}
-\index{Function!Without code}
+\index{Function!Undefined}
 
-The generated program is incorrect for every program which contains a
-memory-related annotation $a$ and a function $f$ without code if and only if:
+The instrumentation in the generated program is partial for a program $p$ if and
+only if $p$ contains a memory-related annotation $a$ and an undefined function
+$f$ such that:
 \begin{itemize}
 \item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
-\item or $a$ is one of the post-condition of $f$.
+\item or $a$ is one of the post-conditions of $f$.
 \end{itemize}
-
-There is no workaround yet.
+A Violation of such an annotation $a$ is undetected. There is no workaround yet.
 
 Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
-functions without code. There is also no workaround yet. 
+undefined functions. There is also no workaround yet.
 
 \section{Recursive Function}
 \index{Function!Recursive}
 
-Programs containing recursive functions have the same limitations than the ones
-containing function without code (Section~\ref{sec:limits:no-code}) and
+Programs containing recursive functions have the same limitations as the ones
+containing undefined functions (Section~\ref{sec:limits:no-code}) and
 memory-related annotations.
 
 Also, even though there is no such annotations, the generated code may call a
-function before it is declared. This behavior appears in a non-specified
-way. The generated code is however easy to fix by hand.
+function before it is declared. When this behavior appears remains
+unspecifed. The generated code is however easy to fix by hand.
 
 \section{Variadic Functions}
 \index{Function!Variadic}
 
-Programs containing variadic functions without code but with a function contract
+Programs containing variadic undefined functions but with a function contract
 are not yet supported. There is no workaround yet.
 
 \section{Function Pointers}
 \index{Function!Pointer}
 
-Programs containing function pointers have the same limitations as about
-memory-related annotations than the ones containing function without code or
+Programs containing function pointers have the same limitations on
+memory-related annotations as the ones containing undefined function or
 recursive functions.
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index 9ef4119884a12d56f43f8f905395940e2831c803..4791b866b0aecb5b31f767f513b44bbede07228b 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/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index a5ed68331eac8e6338be564a1b7ff56f38512acb..a8a26cc583caf07fa1cdead5edda0475d4ce0f94 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -4,15 +4,15 @@ This chapter is the core of this manual and describes how to use the
 plug-in. You can still call the option \optiondef{-}{e-acsl-help} to get the
 list of available options with few lines of documentation. First,
 Section~\ref{sec:simple} shows how to run the plug-in on a toy example and how
-to execute the generated code with a standard \C compiler to detect invalid
+to compile the generated code with a standard \C compiler and to detect invalid
 annotations at runtime. Then, Section~\ref{sec:exec-env} provides additional
 details on the execution of the generated code. Next,
 Section~\ref{sec:incomplete} focuses 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. Section~\ref{sec:combine} explains how to combine the \eacsl plug-in
-with others \framac plug-ins. Finally, Section~\ref{sec:custom} introduces how
-to customize the plug-in, and Section~\ref{sec:verbose} details the verbosing
-policy of the plug-in.
+\emph{i.e.} in which some functions are not defined or in which there are no
+main function. Section~\ref{sec:combine} explains how to combine the \eacsl
+plug-in with other \framac plug-ins. Finally, Section~\ref{sec:custom}
+introduces how to customize the plug-in, and Section~\ref{sec:verbose} details
+the verbosing policy of the plug-in.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -51,7 +51,7 @@ Running \eacsl on this file just consists in adding the option
 
 Even if \texttt{first.i} is already preprocessed, \eacsl first asks the \framac
 kernel to preprocess and to link against \texttt{first.i} several files which
-forms the \eacsl library. Its usefulness will be explain later, mainly in
+form the \eacsl library. Their usage will be explain later, mainly in
 Section~\ref{sec:exec-env}.
 
 Then \eacsl takes the annotated \C code as input and
@@ -61,7 +61,7 @@ translates it into a new \framac project named \texttt{e-acsl}\footnote{The
 nothing more. It is however possible to have a look at the generated code in the
 \framac GUI. This is also possible through the command line thanks to the kernel
 options \optionuse{-}{then-on} and \optionuse{-}{print} which respectively
-switches to another project and pretty prints the \C code~\cite{userman}:
+switch to another project and pretty prints the \C code~\cite{userman}:
 
 \begin{shell}
 \$ frama-c -e-acsl first.i -then-on e-acsl -print
@@ -127,11 +127,10 @@ int main(void)
 
 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 first \eacsl annotation, while the second one is just
-after the second one.
+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. 
 
 \begin{ccode}
   /*@ assert x == 0; */
@@ -145,7 +144,7 @@ which is defined in the \eacsl library. Each call performs the dynamic
 verification that the corresponding assertion is valid. More precisely, it
 checks that its first argument (here \texttt{x == 0} or \texttt{x == 1}) 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}.
+precise error reports as shown in Section~\ref{sec:exec}.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -189,9 +188,9 @@ x == 1.
 \$ echo \$?
 1
 \end{shell}
-This execution stops with an exit code of 1 and an error message indicated that
-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 the second
+This execution stops with exit code 1 and an error message indicating which
+invalid \eacsl annotation has been violated. There is no output for the valid
+\eacsl annotation. So, thanks to the plug-in, we detect that the second
 assertion in the initial program is wrong, while the first one is correct for
 this execution.
 
@@ -202,8 +201,8 @@ this execution.
 \section{Execution Environment of the Generated Code}
 \label{sec:exec-env}
 
-The environment in which the code is executed is not necessarily the same than
-the one assumed by \framac. You must take care of that when running the \eacsl
+The environment in which the code is executed is not necessarily the same as
+the one assumed by \framac. You should take care of that when running the \eacsl
 plug-in and when compiling the generated code with \gcc. In this aspect, the
 plug-in offers a few possibilities of customization.
 
@@ -214,16 +213,16 @@ plug-in offers a few possibilities of customization.
 \index{Runtime Error}
 
 The major difference between \acsl~\cite{acsl} and \eacsl~\cite{eacsl}
-specification languages is that the logic is total in the former language while
-it is partial in the latter one: the semantics of a term denoting a \C
-expression $e$ is undefined if $e$ leads to a runtime error and, consequently,
-the semantics of any term $t$ (resp. predicate $p$) containing such an
-expression $e$ is undefined as soon as $e$ has to be evaluated in order to
-evaluate $t$ (resp. $p$). The \eacsl Reference Manual also states that
-\emph{``it is the responsibility of the tools which interprets \eacsl to ensure
-  that an undefined term is never evaluated''}~\cite{eacsl}.
-
-Accordingly, the \eacsl plug-in prevents undefined terms from being
+specification languages is that the logic is total in the former while it is
+partial in the latter one: the semantics of a term denoting a \C expression $e$
+is undefined if $e$ leads to a runtime error and, consequently, the semantics of
+any term $t$ (resp. predicate $p$) containing such an expression $e$ is
+undefined as soon as $e$ has to be evaluated in order to evaluate $t$
+(resp. $p$). The \eacsl Reference Manual also states that \emph{``it is the
+  responsibility of each tool which interprets \eacsl to ensure that an
+  undefined term is never evaluated''}~\cite{eacsl}.
+
+Accordingly, the \eacsl plug-in prevents an undefined term from being
 evaluated. Should it be because an annotation contains such a term, it will
 report a proper error at runtime instead.
 
@@ -232,9 +231,9 @@ Consider for instance the following annotated program.
 \listingname{rte.i}
 \cinput{examples/rte.i}
 
-The terms and predicates containing the modulo `\%' in the clause
-\texttt{assumes} are undefined in the context of the \texttt{main}'s function
-call since the second argument is equal to 0.
+The terms and predicates containing the modulo `\%' in the \texttt{assumes}
+clause are undefined in the context of the \texttt{main} function call since
+the second argument is equal to 0.
 
 However we can generate an instrumented code and compile it through the
 following command lines:
@@ -244,8 +243,8 @@ following command lines:
 \$ gcc -o rte `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_rte.i
 \end{shell}
 
-Now, when you execute it, you get the following output which explains that your
-function contract is invalid because it contains a division by zero.
+Now, when \texttt{rte} is executed, you get the following output indicating that
+your function contract is invalid because it contains a division by zero.
 
 \begin{shell}
 \$ ./rte
@@ -259,16 +258,16 @@ division_by_zero: y != 0.
 \subsection{Architecture Dependent Annotations}
 
 In many cases, the execution of a \C program depends on the underlying machine
-architecture which it is executed on. The program must be compiled in the very
-same architecture (or cross-compiled) for the compiler being able to generate a
-correct binary.
+architecture it is executed on. The program must be compiled on the very same
+architecture (or cross-compiled for it) for the compiler being able to generate
+a correct binary.
 
 \framac makes assumptions about the machine architecture when analyzing such a
-file. By default, it assumes a x86 32 bits platform, but it may be changed
+file. By default, it assumes an X86 32-bit platform, but it may be customized
 thanks to the option \optionuse{-}{machdep}~\cite{userman}. This option is of
 primary importance when using the \eacsl plug-in: it must be set to the value
-corresponding to the machine which the generated code will be executed on if the
-code \emph{or the annotation} is machine dependent.
+corresponding to the machine architecture which the generated code will be
+executed on if the code \emph{or the annotation} is machine dependent.
 
 Consider for instance the following program.
 
@@ -284,8 +283,8 @@ preprocess the annotations~\cite{userman}):
 \$ gcc -o archi `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_archi.i
 \end{shell}
 
-However, the generated code crashes at runtime on a x86 64 bits computer because
-a 32 bits architecture was assumed at generation time.
+However, the generated code fails at runtime on an X86 64-bit computer because
+a 32-bit architecture was assumed at generation time.
 
 \begin{shell}
 \$ ./archi
@@ -295,7 +294,7 @@ sizeof(long) == 8.
 \end{shell}
 
 There is no assertion failure if you add the option \texttt{-machdep x86\_64}
-when calling \framac.
+when running the \eacsl plug-in.
 
 \begin{shell}
 \$ frama-c -machdep x86_64 -pp-annot -e-acsl archi.c \
@@ -313,7 +312,7 @@ when calling \framac.
 corresponds to mathematical integers. Such a type does 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
+use standard integral types 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.
 
@@ -322,7 +321,7 @@ Consider for instance the following program.
 \listingname{gmp.i}
 \cinput{examples/gmp.i}
 
-Even on a 64 bits machine, it is not possible to compute the assertion with a
+Even on a 64-bit machine, it is not possible to compute the assertion with a
 standard \C type. In this case, the \eacsl plug-in generates \gmp code.
 
 We can generate an instrumented code as usual through the following command
@@ -358,11 +357,11 @@ any integral \C type in an \eacsl annotation.
 
 The \eacsl plug-in handles memory-related annotations such as
 \lstinline|\valid|. When using such an annotation, the generated code must be
-linked against a specific library installed with the plug-in to be
-executed. This library includes two \C files which are installed in the \eacsl'
-share directory:
+linked against a specific memory library installed with the plug-in. 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\_bittree.c}, and
 \item \texttt{memory\_model/e\_acsl\_mmodel.c}.
 \end{itemize}
 
@@ -371,16 +370,16 @@ 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,
+Assuming that we want to execute the generated code on an X86 64-bit machine,
 the generation of the instrumented code requires the use of the option
 \optionuse{-}{machdep} since the code uses \texttt{sizeof}. However, nothing
-more is required here.
+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
+Since the original code uses \lstinline|\valid|, the executable binary
 must be generated from \texttt{monitored\_valid.i} as follows:
 
 \begin{shell}
@@ -390,7 +389,7 @@ must be generated from \texttt{monitored\_valid.i} as follows:
        monitored_valid.i
 \end{shell}
 
-Now we can execute the generate binary which fails at runtime since the second
+Now we can execute the generated binary which fails at runtime since the second
 assertion is violated.
 \begin{shell}
 \$ ./valid
@@ -399,17 +398,18 @@ The failing predicate is:
 freed: \valid(x).
 \end{shell}
 
-Like for integers, the \eacsl plug-in does its best to use the dedicated library
-only when required~\cite{rv13}. So, if your program does not contain
+Like for integers, the \eacsl plug-in does its best to use the dedicated memory
+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, like the examples of the previous
 sections.
 
-However, 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 the \eacsl plug-in inserts runtime checks to prevent them
-according to Section~\ref{sec:runtime-error}, witness the following example.
+However, if your program contains some 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 the \eacsl plug-in inserts runtime checks to prevent
+them according to Section~\ref{sec:runtime-error}, witness the following
+example.
 
 \listingname{pointer.c}
 \cinput{examples/pointer.c}
@@ -428,9 +428,9 @@ mem_access: \valid_read(x).
 \end{shell}
 
 The option \optiondef{-}{e-acsl-full-mmodel} (unset by default) may be set to
-always instrument the code for handling potential memory-related annotations,
-even when it is not required. If it is set, the generated program must be always
-linked against the memory library.
+systematically instrument the code for handling potential memory-related
+annotations, even when it is not required. If it is set, the generated program
+must be always linked against the memory library.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -438,7 +438,7 @@ linked against the memory library.
 
 When a predicate is checked at runtime, the function
 \texttt{e\_acsl\_assert}\codeidxdef{e\_acsl\_assert} is called. Its body is
-defined in the file \texttt{e\_acsl.c} from the \eacsl library. By default, it
+defined in the file \texttt{e\_acsl.c} of the \eacsl library. By default, it
 does nothing if the predicate is valid, while it prints an error message and
 exits (with status 1) if the predicate is invalid.
 
@@ -472,8 +472,10 @@ The verified predicate was: `x == 1'.
 \label{sec:incomplete}
 
 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.
+\eacsl plug-in does not necessarily require to have it to generate the
+instrumented code. It is still possible to instrument a partial program with no
+entry point or in which some functions remain undefined, even though a few
+restrictions.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -521,9 +523,9 @@ x = 65536
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{Functions without Code}
+\subsection{Undefined Functions}
 \label{sec:no-code}
-\index{Function!Without code}
+\index{Function!Undefined}
 
 The \eacsl plug-in may also work if some functions have no implementation.
 Consider for instance the following annotated program for which the
@@ -536,7 +538,7 @@ The instrumented code is generated as usual, even though you get an additional
 warning.
 \begin{shell}
 [e-acsl] beginning translation.
-[e-acsl] warning: annotated function `my_pow' without code:
+[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, 
@@ -573,7 +575,7 @@ the beginning of this manual may overflow in case of large exponentiations.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\section{Combining E-ACSL with Others Plug-ins}
+\section{Combining E-ACSL with Other Plug-ins}
 \label{sec:combine}
 
 As the \eacsl plug-in generates a new \framac project, it is easy to run any
@@ -584,17 +586,17 @@ the generated program uses \gmp or the dedicated memory library: both make
 intensive use of dynamic structures which are usually difficult to handle by
 analysis tools.
 
-Another way to combine \eacsl with others plug-ins is to run \eacsl last.  For
+Another way to combine \eacsl with other plug-ins is to run \eacsl last.  For
 instance, the \rte plug-in~\cite{rte} may be used to generate annotations
 corresponding to runtime errors. Then the \eacsl plug-in may generate an
-instrumented program to verify that there is no such runtime errors during the
+instrumented program to verify that there are no such runtime errors during the
 execution of the program.
 
 Consider the following program.
 
 \listingname{combine.i}
 \cinput{examples/combine.i}
-To check at runtime that this programs does not perform any runtime error (which
+To check at runtime that this program does not perform any runtime error (which
 are potential overflows in this case), just do:
 \begin{shell}
 \$ frama-c -rte combine.i -then -e-acsl -then-on e-acsl -print \
@@ -607,10 +609,10 @@ Nevertheless if you run the \eacsl plug-in after another one, it first generates
 a new temporary project in which it links the analyzed program against its own
 library in order to generate the \framac internal representation of the \C
 program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
-even if the \eacsl plug-in keeps the maximum amount of information, results of
-already executed analyzers (such as the validity status of the 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.
+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
@@ -642,12 +644,12 @@ plug-in is running.
 \section{Customization}
 \label{sec:custom}
 
-There are few 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}.
 
-Second, the directory which the \eacsl library files are searched in -- which is
+Second, the directory where the \eacsl library files are searched in -- which is
 \texttt{`frama-c -print-share-path`/e-acsl} by default -- may be changed by
 setting the option \optiondef{-}{e-acsl-share}.
 
@@ -676,14 +678,14 @@ check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet suppo
 \label{sec:verbose}
 
 By default, \eacsl does not provide much information when it is running. Mainly,
-it prints a message when it begins the translation, and one other when the
+it prints a message when it begins the translation, and another one when the
 translation is done. It may also display warnings when something requires the
 attention of the user, for instance if it is not able to translate an
 annotation. Such information is usually enough but, in some cases, you might
-want to get additional controls on what is displayed. As quite usual with
+want to get additional control on what is displayed. As quite usual with
 \framac plug-ins, \eacsl offers two different ways to do this: the verbosity
 level which indicates the \emph{amount} of information to display, and the
-message categories which indicates the \emph{kind} of information to display.
+message categories which indicate the \emph{kind} of information to display.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -692,7 +694,7 @@ message categories which indicates the \emph{kind} of information to display.
 The amount of information displayed by the \eacsl plug-in is settable by the
 option \optiondef{-}{e-acsl-verbose}. It is 1 by default. Below is indicated
 which information is displayed according to the verbosing level. The level $n$
-also displays the information of the level $n-1$.
+also displays the information of all the lower levels.
 
 \begin{center}
 \begin{tabular}{|l|l|}
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index 5fe9ff11f18b2150629fb847939527a808150b6a..51c7636b1615ecf5c7bf9aad9f45b280e01c3503 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -300,7 +300,7 @@ class dup_functions_visitor prj = object (self)
 	(match g with
 	| GVarDecl _ ->
 	  if vi.vname <> "malloc" && vi.vname <> "free" then
-	    Options.warning "@[annotated function `%a' without code:@ \
+	    Options.warning "@[annotating undefined function `%a':@ \
 the generated program may miss memory instrumentation@ \
 if there are memory-related annotations.@]"
 	    Printer.pp_varinfo vi