From 3056817aeb763cd57ae8729b2396195cc4a36f3c Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 19 Sep 2018 10:24:41 +0200
Subject: [PATCH] [userman] replace section 'Limitations of E-ACSL Monitoring
Libraries' by 'Supported Systems' + improved index
---
src/plugins/e-acsl/doc/userman/changes.tex | 3 +-
.../e-acsl/doc/userman/limitations.tex | 31 +++++++++++++------
src/plugins/e-acsl/doc/userman/macros.tex | 18 +++++------
src/plugins/e-acsl/doc/userman/provides.tex | 7 +++--
4 files changed, 36 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 95adc658f2d..c03e86a05a1 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index f0a488f0f90..6904abf1fb3 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/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.
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index c53111f88fe..f0e91c4d3da 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/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.}}
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 08d1e9aaea3..646e5e34463 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/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
--
GitLab