From 28bbba563cc5ce339672ed10b76c6dfb59e29812 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 8 Oct 2018 09:54:18 +0200
Subject: [PATCH] [userman] fixes according to Fonenantsoa' suggestions
---
src/plugins/e-acsl/doc/userman/biblio.bib | 4 ++--
src/plugins/e-acsl/doc/userman/changes.tex | 8 ++++----
src/plugins/e-acsl/doc/userman/introduction.tex | 5 +++--
src/plugins/e-acsl/doc/userman/limitations.tex | 2 +-
4 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 3b4015a6d13..27d9be4791f 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/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,
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index c03e86a05a1..7ba7552f534 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 0a891902150..1f263c145d1 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/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
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 2ef04f81108..24a3aced3ba 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/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
--
GitLab