diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf
index fe1ac7d29861b3f1992219b2ad2efedc2e944667..8851b13098b0a355d175cb508f9908c183eec1d1 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf
index b4a9bfb6dbed2161525df474b1055de4a06c9c42..38e97aed810c91fc7a9b42167a98a9ffff8cafd7 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index c6f936ac8ce3bbb75e66cc6619397b0def464058..534e9878a1508c5c79d1dd6786ef31350edbc77d 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -6,7 +6,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 memory_modern.bnf \
+ loc_modern.bnf memory_modern.bnf list-gram.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 \
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 015978d8b81bdd6ae641c50736d3b74b7c8ce369..d79c15855c9149c27dfe53bf575d13b42f6eca3a 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -1,28 +1,41 @@
\section{Changes}
-\subsection{Version \version}
+\subsection*{Version \version}
+\begin{itemize}
+\item Update according to \acsl 1.12:
+ \begin{itemize}
+ \item \changeinsection{locations}{add subsections for build-in lists}
+ \item \changeinsection{statement_contract}{fix syntax rule for statement
+ contracts in allowing completeness clauses}
+ \item \changeinsection{memory}{add syntax for defining a set by giving
+ explicitely its element}
+ \item \changeinsection{typedpointers}{new section}
+ \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.9}
\begin{itemize}
-\item \changeinsection{alloc-dealloc}{include this section}
+\item \changeinsection{alloc-dealloc}{new section}
\item Update according to \acsl 1.9.
\end{itemize}
-\subsection{Version 1.8}
+\subsection*{Version 1.8}
\begin{itemize}
-\item \changeinsection{locations}{Fix example \ref{ex:tset}}
-\item \changeinsection{pointers}{Add grammar of memory-related terms and
+\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}
+\subsection*{Version 1.7}
\begin{itemize}
\item Update according to \acsl 1.7.
\item \changeinsection{separation}{no more absent}
\end{itemize}
-\subsection{Version 1.5-4}
+\subsection*{Version 1.5-4}
\begin{itemize}
\item Fix typos.
@@ -36,7 +49,7 @@
in \lstinline|\\at|}
\end{itemize}
-\subsection{Version 1.5-3}
+\subsection*{Version 1.5-3}
\begin{itemize}
\item Fix various typos.
@@ -49,7 +62,7 @@ in \lstinline|\\at|}
\item \changeinsection{logicalstates}{add hybrid functions and predicates}
\end{itemize}
-\subsection{Version 1.5-2}
+\subsection*{Version 1.5-2}
\begin{itemize}
\item \changeinsection{expressions}{remove laziness of operator
@@ -62,7 +75,7 @@ in \lstinline|\\at|}
add example.}
\end{itemize}
-\subsection{Version 1.5-1}
+\subsection*{Version 1.5-1}
\begin{itemize}
\item Fix many typos.
@@ -82,7 +95,7 @@ in \lstinline|\\at|}
\item \changeinsection{specmodules}{add specification modules}
\end{itemize}
-\subsection{Version 1.5-0}
+\subsection*{Version 1.5-0}
\begin{itemize}
\item Initial version.
@@ -95,20 +108,20 @@ in \lstinline|\\at|}
{
\section{Changes in \eacsl Implementation}
-\subsection{Version \eacslversion}
+\subsection*{Version \eacslversion}
\begin{itemize}
\item \changeinsection{alloc-dealloc}{support of
\lstinline|\\freeable|}
\end{itemize}
-\subsection{Version 0.3}
+\subsection*{Version 0.3}
\begin{itemize}
\item \changeinsection{loop_annot}{support of loop invariant}
\end{itemize}
-\subsection{Version 0.2}
+\subsection*{Version 0.2}
\begin{itemize}
\item \changeinsection{expressions}{support of bitwise complementation}
@@ -119,7 +132,7 @@ in \lstinline|\\at|}
\item \changeinsection{dangling}{support of \lstinline|\\initialized|}
\end{itemize}
-\subsection{Version 0.1}
+\subsection*{Version 0.1}
\begin{itemize}
\item Initial version.
diff --git a/src/plugins/e-acsl/doc/refman/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
index 8aae7b9eff6f2de6fe20ee0bd3a55415809a6389..609006e8f99bb55b3a7dd87eabf18f5f8096c022 100644
--- a/src/plugins/e-acsl/doc/refman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -1 +1 @@
-\newcommand{\eacslversion}{0.5}
+\newcommand{\eacslversion}{0.8}
diff --git a/src/plugins/e-acsl/doc/refman/list-gram.tex b/src/plugins/e-acsl/doc/refman/list-gram.tex
new file mode 100644
index 0000000000000000000000000000000000000000..de081932cead22daf4ba87f59ca580258a1fff98
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/list-gram.tex
@@ -0,0 +1,7 @@
+\begin{syntax}
+ term ::= "[|" "|]" ; empty list
+ | "[|" term ("," term)* "|]" ; list of elements
+ | term "^" term ; list concatenation (overloading bitwise-xor
+ ; operator)
+ | term "*^" term ; list repetition
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/loc.tex b/src/plugins/e-acsl/doc/refman/loc.tex
index 23fbf3635333081f7164e4636227fbf5f204a2c1..f998e26dc08ca39989904fb0beae5a8ef8f9743a 100644
--- a/src/plugins/e-acsl/doc/refman/loc.tex
+++ b/src/plugins/e-acsl/doc/refman/loc.tex
@@ -10,8 +10,10 @@
| { "\inter" "(" tset ("," tset)* ")" }; intersection
| tset "+" tset ;
| "(" tset ")" ;
- | [ { "{" tset "|" binder ";" guards ("&&" pred)? "}" } ]; set comprehension
- | { "{" term "}" } ; explicit singleton
+ | {[the given term cannot itself be a set]
+ "{" tset "|" binders (";" pred)? "}"} ; set comprehension
+ | {[the given terms cannot themselves be a set]
+ "{" (tset ("," tset)*)? "}" };
| term ; implicit singleton
\
pred ::= { "\subset" "(" tset "," tset ")" } ; set inclusion
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 0a3803d504811c87c38ecceb411af61a4f3ba270..754211277a2fb0a7d8ec45365802b2c743a64f57 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -24,7 +24,7 @@
\usepackage{alltt}
\makeindex
-\newcommand{\acslversion}{1.9\xspace}
+\newcommand{\acslversion}{1.12\xspace}
\newcommand{\version}{\acslversion\xspace}
\renewcommand{\textfraction}{0.01}
@@ -55,9 +55,10 @@
CEA LIST, Software Reliability Laboratory\\
\vfill
\begin{flushleft}
- \textcopyright 2011-2013 CEA LIST
+ \textcopyright 2011-2017 CEA LIST
- This work has been supported by the `Hi-Lite' FUI project (FUI AAP 9).
+ This work has been initially supported by the `Hi-Lite' FUI project (FUI AAP
+ 9).
\end{flushleft}
\end{titlepage}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index a9d2e139285eac9ea8f1c23579f40209c8a97c2e..b868b10cdbd1e0126378107056d8fb430ae2eaf0 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -694,10 +694,24 @@ evolve in the future.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Sets as first-class values}
+\section{Sets and lists}
\index{location}
+
+\subsection{Finite sets}
+\nodiff
+
+\subsection{Finite lists}
\nodiff
+Figure~\ref{fig:gram:list} shows the notations for built-in lists.
+\begin{figure}[t]
+ \begin{cadre}
+ \input{list-gram.bnf}
+ \end{cadre}
+ \caption{Notations for built-in list datatype}
+\label{fig:gram:list}
+\end{figure}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -792,3 +806,11 @@ same than the one of \acsl.
\difficultswhy{\lstinline|\\initialized| and
\notimplemented{\lstinline|\\dangling|}}{the implementation of a memory
model}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Well-typed pointers}
+\label{sec:typedpointers}
+\absentexperimental
diff --git a/src/plugins/e-acsl/doc/refman/st_contracts.tex b/src/plugins/e-acsl/doc/refman/st_contracts.tex
index 7e574f5690e265a62b7c218c0d00b9928894e779..498e9a73899ed7fd58fe49dfa210018d10d93964 100644
--- a/src/plugins/e-acsl/doc/refman/st_contracts.tex
+++ b/src/plugins/e-acsl/doc/refman/st_contracts.tex
@@ -2,5 +2,11 @@
statement ::= "/*@" statement-contract "*/" statement
\
[ statement-contract ] ::= {("for" id ("," id)* ":")?} requires-clause* ;
- simple-clause* behavior-body*
+ simple-clause* named-behavior-stmt* ;
+ completeness-clause*
+ \
+ named-behavior-stmt ::= "behavior" id ":" behavior-body-stmt
+ \
+ behavior-body-stmt ::= assumes-clause* ;
+ requires-clause* simple-clause-stmt*
\end{syntax}