[refman] update wrt ACSL v1.12

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 \

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

 \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.

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

-\newcommand{\eacslversion}{0.5}
+\newcommand{\eacslversion}{0.8}

src/plugins/e-acsl/doc/refman/list-gram.tex

+\begin{syntax}
+  term ::=  "[|" "|]" ; empty list
+       | "[|" term ("," term)* "|]" ; list of elements
+       | term "^" term ; list concatenation (overloading bitwise-xor 
+                         ; operator)
+       | term "*^" term ; list repetition
+\end{syntax}

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

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}
 

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

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}