From 7935097adb3f38e515d7dccd2257e52c2439cad4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 7 Mar 2014 14:31:23 +0100
Subject: [PATCH] [doc] update reference manual and add a missing figure
---
src/plugins/e-acsl/.gitignore | 1 +
src/plugins/e-acsl/doc/refman/.gitignore | 1 +
src/plugins/e-acsl/doc/refman/Makefile | 10 ++++---
.../e-acsl/doc/refman/changes_modern.tex | 2 ++
.../e-acsl/doc/refman/eacslversion.tex | 2 +-
.../e-acsl/doc/refman/macros_modern.tex | 2 +-
src/plugins/e-acsl/doc/refman/main.tex | 7 +++--
src/plugins/e-acsl/doc/refman/memory.tex | 27 +++++++++++++++++++
.../e-acsl/doc/refman/speclang_modern.tex | 18 ++++++++++---
9 files changed, 56 insertions(+), 14 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/refman/memory.tex
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index fd9f25d08ed..3ccc328577b 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 a2c62a9667f..b7b857f4e79 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 2e6e31df15a..d7d568db15d 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 0a33be177e0..e2b407e15a0 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 bcd7fed2736..8eacf0ee12c 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 51719d3d384..c0a25d556aa 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 486e255d88c..6b41fe4bddb 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 00000000000..863199e5275
--- /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 3079971445f..71de79df786 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}
--
GitLab