[doc] update reference manual and add a missing figure

src/plugins/e-acsl/.gitignore

+*~
 /*.o
 /*.cm*
 /*.annot

src/plugins/e-acsl/doc/refman/.gitignore

 e-acsl.pdf
+e-acsl-implementation.pdf

src/plugins/e-acsl/doc/refman/Makefile

@@ -4,7 +4,7 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
 	libraries_modern.tex concl_modern.tex changes_modern.tex \
 	term_modern.bnf binders_modern.bnf predicate_modern.bnf \
 	fn_behavior_modern.bnf oldandresult_modern.bnf \
-	loc_modern.bnf \
+	loc_modern.bnf memory_modern.bnf \
 	assertions_modern.bnf loops_modern.bnf st_contracts_modern.bnf \
 	logic_modern.bnf data_invariants_modern.bnf model_modern.bnf \
 	ghost_modern.bnf generalinvariants_modern.bnf iterator_modern.bnf \
@@ -18,8 +18,8 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
 
 all: e-acsl
 
-LANGUAGE_VERSION=1.7-1
-EACSL_VERSION= 0.3
+LANGUAGE_VERSION=1.8
+EACSL_VERSION= 0.4
 
 EACSL_DIR=../..
 DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
@@ -106,7 +106,9 @@ e-acsl.pdf: $(DEPS_MODERN)
 
 e-acsl.tex: e-acsl-implementation.tex Makefile
 	rm -f $@
-	sed -e '/PrintImplementationRq/s/%--//' $^ > $@
+	sed -e '/PrintImplementationRq/s/%--//' \
+	    -e '/ColorImplementationRq/s/%--//' \
+	    $^ > $@
 	chmod a-w $@
 
 # version pour le goupe de travail E-ACSL

src/plugins/e-acsl/doc/refman/changes_modern.tex

@@ -4,6 +4,8 @@
 
 \begin{itemize}
 \item \changeinsection{locations}{Fix example \ref{ex:tset}}
+\item \changeinsection{pointers}{Add grammar of memory-related terms and
+  predicates}
 \end{itemize}
 
 \subsection{Version 1.7}

src/plugins/e-acsl/doc/refman/eacslversion.tex

-\newcommand{\eacslversion}{0.3}
+\newcommand{\eacslversion}{0.4}

src/plugins/e-acsl/doc/refman/macros_modern.tex

@@ -106,7 +106,7 @@
 %%% Commandes et environnements pour la version relative  l'implementation
 \newcommand{\highlightnotimplemented}{%
 \ifthenelse{\boolean{ColorImplementationRq}}{\color{red}}%
-           {\ul}%
+           {}%
 }%
 
 \newcommand{\notimplemented}[2][]{%

src/plugins/e-acsl/doc/refman/main.tex

@@ -12,8 +12,7 @@
 %Do not touch the following line. It is used in a Makefile hack to
 %produce the ACSL document shipped with the Frama-C distribution.
 %--\setboolean{PrintImplementationRq}{false}
-
-%\setboolean{ColorImplementationRq}{false}
+%--\setboolean{ColorImplementationRq}{false}
 
 \usepackage{amssymb}
 \usepackage{graphicx}
@@ -25,8 +24,8 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\acslversion}{1.7\xspace}
-\newcommand{\version}{\acslversion-1\xspace}
+\newcommand{\acslversion}{1.8\xspace}
+\newcommand{\version}{\acslversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
 \renewcommand{\topfraction}{0.99}

src/plugins/e-acsl/doc/refman/memory.tex

+\begin{syntax}
+  term ::= "\null" ;
+        | "\base_addr" { one-label? } "(" term ")" ;
+        | "\block_length" { one-label? } "(" term ")" ;
+        | "\offset" { one-label? } "(" term ")" ;
+        | { "\allocation" one-label? "(" term ")" };
+       \
+  pred ::= { "\allocable" one-label? "(" term ")" };
+       |  { "\freeable" one-label? "(" term ")" };
+       | { "\fresh" two-labels? "(" term, term ")" };
+       | "\valid" { one-label? } "(" location-address ")" ;
+       | "\valid_read" { one-label? } "(" location-address ")";
+       | { "\separated" "(" location-address "," location-addresses ")" };
+       \
+  { one-label } ::= { "{" id "}" } ;
+       \
+  { two-labels } ::= { "{" id, id "}" } ;
+       \
+  location-addresses ::= location-address ("," location-address)*
+  \
+  location-address ::= tset
+\end{syntax}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End:

src/plugins/e-acsl/doc/refman/speclang_modern.tex

@@ -77,8 +77,8 @@ this form of quantifier is limited to \texttt{integer} and its subtype. Thus
 there is no guarded quantification over \texttt{float}, \texttt{real}, \C
 pointers or logic types.
 
-\item[\notimplemented{Iterator quantification}] In order to iterate over
-  non-integer types, \eacsl introduces a notion of $iterators$ over types:
+\item[{\highlightnotimplemented{Iterator quantification}}] In order to iterate
+  over non-integer types, \eacsl introduces a notion of $iterators$ over types:
   standard \acsl unguarded quantifications are only allowed over a type which an
   iterator is attached to.
 
@@ -111,8 +111,8 @@ pointers or logic types.
     \cinput{link.c}
   \end{example}
 
-\item[\notimplemented{Unguarded quantification}] They are only allowed over
-  boolean and char. 
+\item[{\highlightnotimplemented{Unguarded quantification}}] They are only
+  allowed over boolean and char.
 \end{description}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -652,6 +652,16 @@ axiomatics.
 
 \except{separation, allocation and deallocation is unsupported}
 
+Figure~\ref{fig:gram:memory} shows the additional constructs for terms and
+predicates which are related to memory location.
+\begin{figure}[htbp]
+  \fbox{\begin{minipage}{0.97\linewidth}
+      \input{memory_modern.bnf}
+    \end{minipage}}
+  \caption{Grammar extension of terms and predicates about memory}
+\label{fig:gram:memory}
+\end{figure}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Memory blocks and pointer dereferencing}