From fff9e61986c323960e32dc04041ea30b22c276a0 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 18 Sep 2018 15:09:26 +0200
Subject: [PATCH] [refman] support of ranges
---
src/plugins/e-acsl/VERSION | 2 +-
src/plugins/e-acsl/doc/Changelog | 3 ++-
src/plugins/e-acsl/doc/refman/.gitignore | 1 +
src/plugins/e-acsl/doc/refman/changes_modern.tex | 15 +++++++++++++++
src/plugins/e-acsl/doc/refman/loc.tex | 3 ++-
src/plugins/e-acsl/doc/refman/loops.tex | 4 ++--
src/plugins/e-acsl/doc/refman/main.tex | 2 +-
src/plugins/e-acsl/doc/refman/speclang_modern.tex | 14 +++++++++++++-
8 files changed, 37 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 076eace285b..78c3791c9d4 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-Chlorine-20180501-beta
+Chlorine-20180501+dev
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3f9ccc57028..3a70cdfe5a9 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,7 +19,8 @@
# configure configure
###############################################################################
-- E-ACSL [2018/18/09] Support for ranges in a few builtins.
+- E-ACSL [2018/18/09] Support for ranges in memory builtins
+ (\valid, \initialized, etc).
###############################
Plugin E-ACSL Chlorine-20180501
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index b7b857f4e79..2c2b06ea711 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -1,2 +1,3 @@
e-acsl.pdf
e-acsl-implementation.pdf
+eacslversion.tex
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 8adaf7b0066..99a5c9360d6 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,14 @@
\subsection*{Version \version}
\begin{itemize}
+\item Update according to \acsl 1.13:
+ \begin{itemize}
+ \item \changeinsection{locations}{add syntax for set membership}
+ \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.12}
+\begin{itemize}
\item Update according to \acsl 1.12:
\begin{itemize}
\item \changeinsection{locations}{add subsections for build-in lists}
@@ -110,6 +118,13 @@ in \lstinline|\\at|}
\subsection*{Version \eacslversion}
+\begin{itemize}
+\item \changeinsection{locations}{support of ranges in memory built-ins
+ (e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
+\end{itemize}
+
+\subsection*{Version Chlorine-20180501}
+
\begin{itemize}
\item \changeinsection{expressions}{support of \lstinline|\\let| binding}
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/loc.tex b/src/plugins/e-acsl/doc/refman/loc.tex
index f998e26dc08..37cdb3a22a2 100644
--- a/src/plugins/e-acsl/doc/refman/loc.tex
+++ b/src/plugins/e-acsl/doc/refman/loc.tex
@@ -5,7 +5,7 @@
| "*" tset ;
| "&" tset ;
| tset "[" tset "]" ;
- | [ { term ".." term } ] ; range
+ | [ term ".." term ] ; range
| { "\union" "(" tset ("," tset)* ")" } ; union of locations
| { "\inter" "(" tset ("," tset)* ")" }; intersection
| tset "+" tset ;
@@ -17,4 +17,5 @@
| term ; implicit singleton
\
pred ::= { "\subset" "(" tset "," tset ")" } ; set inclusion
+ | { term "\in" tset } ; set membership
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 3294e626298..5d1fa33003c 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -21,8 +21,8 @@
{ loop-assigns } ::= { "loop" "assigns" locations ";" } ;
\
{ loop-behavior } ::= { "for" id ("," id)* ":" } ;
- { loop-clause* } ; annotation for behavior $id$
+ { loop-clause* } ; \hspace{-30mm} annotation for behavior $id$
\
{ loop-variant } ::= { "loop" "variant" term ";" } ;
- | { "loop" "variant" term "for" id ";" } ; variant for relation $id$
+ | { "loop" "variant" term "for" id ";" } ; \hspace{-30mm} variant for relation $id$
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 8914df96cd7..fb3dabe02dc 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.12\xspace}
+\newcommand{\acslversion}{1.13\xspace}
\newcommand{\version}{\acslversion\xspace}
\renewcommand{\textfraction}{0.01}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index c2ee3338b80..2b4fa7dec49 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -374,6 +374,17 @@ set of all integers between 0 and 9 and between 20 and 29.
\end{example}
\end{notimplementedenv}
+\begin{notimplementedenv}
+ Ranges are currently only supported in memory built-ins described in
+ Section~\ref{subsec:memory} and~\ref{sec:dangling}.
+
+\begin{example}
+The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that
+the ten first cells of the array \lstinline|t| are valid. Writing the term
+\lstinline|&t[0 .. 9]| alone, outside any memory built-in, is not yet supported.
+\end{example}
+\end{notimplementedenv}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Default contracts, multiple contracts}
@@ -665,7 +676,8 @@ predicates which are related to memory location.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Memory blocks and pointer dereferencing}
-\label{subsec:memory}\label{sec:memory}
+\label{subsec:memory}
+\label{sec:memory} % for correctness of \changeinsection in Changes
\nodiff
\difficultswhy{\lstinline|\\base\_addr|,
--
GitLab