diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index fd9f25d08edc7e2c5a8cb881034109122baf471f..3ccc328577bdc92ea5995d33e33a03852983c04f 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -1,3 +1,4 @@
+*~
/*.o
/*.cm*
/*.annot
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index a2c62a9667fc6ccbdd9fcbe7243ffa8c55a56964..b7b857f4e7925cce8eecab9571078c72bb404444 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -1 +1,2 @@
e-acsl.pdf
+e-acsl-implementation.pdf
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 2e6e31df15a05d0ff252af2ee900901c34e37234..d7d568db15dd19df2975c0273f5058bd842dd268 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/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
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 0a33be177e00f7941251fd59f5c2279bd45ab1b1..e2b407e15a02f66b65697f34c83ebbf1d4840def 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/refman/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
index bcd7fed2736b657802155bcd2c7166854a3bb46b..8eacf0ee12c8f5c79dec65a1ebc5094e460dc601 100644
--- a/src/plugins/e-acsl/doc/refman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -1 +1 @@
-\newcommand{\eacslversion}{0.3}
+\newcommand{\eacslversion}{0.4}
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
index 51719d3d384b090aface34a61becfd4faa963e13..c0a25d556aa20064bd9f4384fbbfca0e0eaafe18 100644
--- a/src/plugins/e-acsl/doc/refman/macros_modern.tex
+++ b/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][]{%
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 486e255d88cc2be55ba453aab90828aa19fa7055..6b41fe4bddb49c73557c5dbaaaff2ff6fb77ca8d 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/refman/memory.tex b/src/plugins/e-acsl/doc/refman/memory.tex
new file mode 100644
index 0000000000000000000000000000000000000000..863199e5275dd5d195d156121c6875d2ea220eea
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/memory.tex
@@ -0,0 +1,27 @@
+\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:
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 3079971445ff6a6a33ac372bf62e5fd991d46ba7..71de79df78646bec39e0e573533827c748036b15 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/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}