[userman] fixes according to Fonenantsoa' suggestions

src/plugins/e-acsl/doc/userman/biblio.bib

@@ -61,9 +61,9 @@
 
 @inproceedings{rvcubes17tool,
   author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
-  title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C 
+  title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
 Programs. Tool Paper}},
-  booktitle = {International Workshop on Competitions, Usability, Benchmarks, 
+  booktitle = {International Workshop on Competitions, Usability, Benchmarks,
 Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)},
   year = 2017,
   month = sep,

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

@@ -13,12 +13,12 @@ release. First we list changes of the last release.
 
 \begin{itemize}
 \item \textbf{Introduction}: Improve a bit and reference related papers.
-\item \textbf{Wat the Plug-in Provides}: Highlight that the memory analysis is
+\item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
   not yet robust.
-\item \textbf{Wat the Plug-in Provides}: Highlight the importance of
+\item \textbf{What the Plug-in Provides}: Highlight the importance of
   \textbf{-e-acsl-prepare}.
-\item \textbf{Known Limitations}: Add the section ``Supported Systems'' that
-  replaces the former section ``Limitations of E-ACSL Monitoring Libraries''.
+\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
+  Monitoring Libraries'' by the new section ``Supported Systems''.
 \end{itemize}
 
 \section*{E-ACSL Chlorine-20180501}

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

@@ -14,7 +14,8 @@ program.
 \C code and perform what is usually referred to as ``runtime assertion
 checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
   annotation checking'' would be more precise.}. This is the primary goal of
-\eacsl. Indirectly, in combination with plug-in \rte~\cite{rte} of \framac, this
+\eacsl. Indirectly, in combination with the \rte plug-in~\cite{rte} of \framac,
+this 
 usage allows the user to detect undefined behaviors in its \C code. Second, it
 allows to combine \framac and its existing analyzers with other \C analyzers
 that do not natively understand the \acsl specification language. Third, the
@@ -23,7 +24,7 @@ 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 assertions that cannot be verified statically and
 thus to establish a link between runtime monitoring and static analysis tools
-such as \Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}. 
+such as \Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}.
 
 Annotations used by the plug-in must be written in the \eacsl specification
 language~\cite{eacsl,sac13} -- a subset of \acsl. \eacsl plug-in is still in a

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

@@ -20,7 +20,7 @@ The only well-supported system is a Linux distribution on a 64-bit architecture.
 
 \subsection{Operating Systems}
 
-Not-Linux systems are almost not yet experimented. It might work but there are
+Non-Linux systems are almost not yet experimented. It might work but there are
 most probably issues, in particular if using a non-standard
 libc\index{Libc}. For instance, there are known bugs under Mac OS
 X\index{Mac OS X}\footnote{See for instance at