[userman] replace section 'Limitations of E-ACSL Monitoring Libraries' by...

[userman] replace section 'Limitations of E-ACSL Monitoring Libraries' by 'Supported Systems' + improved index

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

@@ -17,7 +17,8 @@ release. First we list changes of the last release.
   not yet robust.
 \item \textbf{Wat the Plug-in Provides}: Highlight the importance of
   \textbf{-e-acsl-prepare}.
-\item \textbf{Known Limitations}: Only support little-endian.
+\item \textbf{Known Limitations}: Add the section ``Supported Systems'' that
+  replaces the former section ``Limitations of E-ACSL Monitoring Libraries''.
 \end{itemize}
 
 \section*{E-ACSL Chlorine-20180501}

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

@@ -12,6 +12,27 @@ 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{Supported Systems}
+
+\begin{important}
+The only well-supported system is a Linux distribution on a 64-bit architecture.
+\end{important}
+
+\subsection{Operating Systems}
+
+Not-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
+  \url{https://bts.frama-c.com/view.php?id=2369}}.
+
+\subsection{Architectures and Runtime Library}
+
+The segment-based memory model (used by default for monitoring memory properties
+such as \lstinline|\valid|) assumes little-endian architecture and has very
+limited support for 32-bit architectures. When using a 32-bit machine or
+big-endians, we recomend using the bittree-based memory model instead.
+
 \section{Uninitialized Values}
 \index{Uninitialized value}
 
@@ -177,13 +198,3 @@ POSIX-compliant memory management functions
 listed above. Monitoring of programs that allocate memory using non-standard or
 obsolete functions (e.g., \T{valloc}, \T{memalign}, \T{pvalloc}) may not work
 correctly.
-
-\section{Limitations of E-ACSL Monitoring Libraries}
-\index{Function!Libraries}
-
-\eacsl monitoring library implementing segment-based memory model is fairly
-recent and presently has very limited support for 32-bit architectures.  When
-using a 32-bit machine we recommend using the bittree-based memory model
-instead.
-
-This library also assumes a little-endian architecture.

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

@@ -5,19 +5,19 @@
 \usepackage{comment}
 
 \newcommand{\framac}{\textsc{Frama-C}\xspace}
-\newcommand{\acsl}{\textsc{ACSL}\xspace}
+\newcommand{\acsl}{\textsc{ACSL}\index{ACSL}\xspace}
 \newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
 \newcommand{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
-\newcommand{\rte}{\textsc{RTE}\xspace}
+\newcommand{\rte}{\textsc{RTE}\index{RTE}\xspace}
 \newcommand{\C}{\textsc{C}\xspace}
-\newcommand{\jml}{\textsc{JML}\xspace}
-\newcommand{\Eva}{\textsc{Eva}\xspace}
-\newcommand{\variadic}{\textsc{Variadic}\xspace}
-\newcommand{\wpplugin}{\textsc{Wp}\xspace}
-\newcommand{\pathcrawler}{\textsc{PathCrawler}\xspace}
+\newcommand{\jml}{\textsc{JML}\index{JML}\xspace}
+\newcommand{\Eva}{\textsc{Eva}\index{Eva}\xspace}
+\newcommand{\variadic}{\textsc{Variadic}\index{Variadic}\xspace}
+\newcommand{\wpplugin}{\textsc{Wp}\index{WP}\xspace}
+\newcommand{\pathcrawler}{\textsc{PathCrawler}\index{PathCrawler}\xspace}
 \newcommand{\gcc}{\textsc{Gcc}\xspace}
-\newcommand{\gmp}{\textsc{GMP}\xspace}
-\newcommand{\dlmalloc}{\textsc{dlmalloc}\xspace}
+\newcommand{\gmp}{\textsc{GMP}\index{GMP}\xspace}
+\newcommand{\dlmalloc}{\textsc{dlmalloc}\index{dlmalloc}\xspace}
 
 \newcommand{\nodiff}{\emph{No difference with \acsl.}}
 \newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}

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

@@ -398,7 +398,7 @@ It might be particularly useful in one of the following contexts:
   verifying them (for instance, only checking undefine behaviors matters).
 \end{itemize}
 
-\begin{important} \index{eacslgcc}
+\begin{important}
 Notably, \eacslgcc disables \framac libc by default. This is because most of
 its functions are annotated with \eacsl contracts and generating code for
 these contracts results in additional runtime overheads. To enforce default
@@ -899,8 +899,9 @@ known in this new project.
 \begin{important}
 If you want to keep results of former analysis, you have to set the option
 \shortopt{e-acsl-prepare} when the first analysis is asked for. The standard
-example is running \eacsl after \Eva: in such a case, \shortopt{e-acsl-prepare}
-must be provided together with the \Eva's \shortopt{-val} option.
+example is running \eacsl after \Eva\index{Eva}: in such a case,
+\shortopt{e-acsl-prepare} must be provided together with the \Eva's
+\shortopt{val} option.
 \end{important}
 
 In this context, the \eacsl plug-in does not generate code for annotations