[eacsl:doc] Update E-ACSL reference manual

- Function contracts: remove abrupt clauses from the list of exceptions
- Statement contracts: remove abrupt clauses from the list of exceptions
- Add grammar for abrupt termination
- Update list of contributors

src/plugins/e-acsl/doc/refman/Makefile

@@ -15,7 +15,7 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
 	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 \
-	bsearch.c bsearch2.c link.c
+	abrupt_modern.bnf bsearch.c bsearch2.c link.c
 
 ##############
 # Main rules #

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

+\begin{syntax}
+    { abrupt-clause } ::= { exits-clause }
+    \
+    { exits-clause } ::= { "exits" pred ";" }
+    \
+    { abrupt-clause-stmt } ::= { breaks-clause } | { continues-clause } | { returns-clause }
+    \
+    { breaks-clause } ::= { "breaks" pred ";" }
+    \
+    { continues-clause } ::= { "continues" pred ";" }
+    \
+    { returns-clause } ::= { "returns" pred ";" }
+    \
+    { term } ::= { "\exit_status" }
+  \end{syntax}

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

@@ -61,7 +61,7 @@
 \item \changeinsection{typing}{no user-defined types}
 \item \changeinsection{builtinconstructs}{no more implementation issue for
   \lstinline|\\old|}
-\item \changeinsection{at}{more restrictive scoping rule for label references 
+\item \changeinsection{at}{more restrictive scoping rule for label references
 in \lstinline|\\at|}
 \end{itemize}
 
@@ -84,7 +84,7 @@ in \lstinline|\\at|}
 \item \changeinsection{expressions}{remove laziness of operator
   \lstinline|<==>|}
 \item \changeinsection{expressions}{restrict guarded quantifications to integer}
-\item \changeinsection{expressions}{add iterator quantifications} 
+\item \changeinsection{expressions}{add iterator quantifications}
 \item \changeinsection{expressions}{extend unguarded quantifications to char}
 \item \changeinsection{locations}{extend syntax of set comprehensions}
 \item \changeinsection{loop_annot}{simplify explanations for loop invariants and
@@ -128,6 +128,11 @@ in \lstinline|\\at|}
 
 \begin{itemize}
 \item \changeinsection{reals}{support of rational numbers and operations}
+\item \changeinsection{fn-behavior}{remove abrupt clauses from the list of
+  exceptions}
+\item \changeinsection{statement_contract}{remove abrupt clauses from the list
+  of exceptions}
+\item \changeinsection{abrupt}{add grammar for abrupt termination}
 \end{itemize}
 
 \subsection*{Version Potassium-19}

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

 \begin{syntax}
-  [ function-contract ] ::= requires-clause*;
-                            { decreases-clause? } simple-clause*;
+  [ function-contract ] ::= requires-clause*
+                            { decreases-clause? } simple-clause*
                             named-behavior* { completeness-clause* }
   \
   requires-clause ::= "requires" pred ";"
@@ -8,6 +8,7 @@
   { decreases-clause } ::= { "decreases" term ("for" id)? ";" }
   \
   [ simple-clause ] ::= { assigns-clause } | ensures-clause
+                        | { allocation-clause} | { abrupt-clause }
   \
   { assigns-clause } ::= { "assigns" locations ";" }
   \

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

@@ -43,7 +43,7 @@ currently implemented into the \framac's \eacsl plug-in.
   \begin{center}
     \begin{tabular}{|l|l|}
       \hline
-      typing 
+      typing
       & mathematical reals \\
       \hline
       terms
@@ -52,7 +52,7 @@ currently implemented into the \framac's \eacsl plug-in.
       & let binding \\
       & t-sets \\
       \hline
-      predicates 
+      predicates
       & exclusive or operator \\  %     \lstinline|^^|
       & let bindings \\
       & quantifications over non-integer types \\
@@ -60,7 +60,7 @@ currently implemented into the \framac's \eacsl plug-in.
       & \lstinline|\\specified|
       \\
       \hline
-      annotations 
+      annotations
       & behavior-specific annotations \\
       & loop assigns \\
       & loop variants \\
@@ -69,6 +69,7 @@ currently implemented into the \framac's \eacsl plug-in.
       \hline
       behavior clauses
       & assigns \\
+      & allocates \\
       & decreases \\
       & abrupt termination \\
       & complete and disjoint behaviors

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

@@ -82,6 +82,7 @@ Patrick Baudin,
 Bernard Botella,
 Lo\"ic Correnson,
 Pascal Cuoq,
+Basile Desloges,
 Johannes Kanig,
 Fonenantsoa Maurica,
 David Mentr\'e,

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

@@ -196,7 +196,7 @@ one is valid:
 \item \lstinline|\exists integer x, 1 <= x <= 0 && -1 <= 1/x <= 1|
 \end{itemize}
 In particular, the second one is invalid since the quantification is in fact an
-enumeration over a finite number of elements, it amounts to 
+enumeration over a finite number of elements, it amounts to
 \lstinline|1/-1 > 0 && 1/0 > 0 && 1/1 > 0|. The first atomic proposition is
 invalid, so the rest of the conjunction (and in particular 1/0) is not
 evaluated. The fourth one is invalid since it is an existential quantification
@@ -294,13 +294,12 @@ It is not possible to define logic types introduced by the specification writer
 \label{sec:fn-behavior}
 \index{function contract}\index{contract}
 
-\except{no \lstinline|terminates| and \lstinline|abrupt| clauses}
+\except{no \lstinline|terminates|}
 
 Figure~\ref{fig:gram:contracts} shows grammar of function
 contracts. This is a simplified version of \acsl one without
-\lstinline|terminates| and \lstinline|abrupt|
-clauses. Section~\ref{sec:termination} (resp.~\ref{sec:abrupt}) explains why
-\eacsl has no \lstinline|terminates| (resp. \lstinline|abrupt|) clause.
+\lstinline|terminates| clauses. Section~\ref{sec:termination} explains why
+\eacsl has no \lstinline|terminates| clause.
 
 \begin{figure}[htbp]
   \begin{cadre}
@@ -370,7 +369,7 @@ members easily identifiable.
 
 \begin{notimplementedenv}
 \begin{example}\label{ex:tset}
-The set \lstinlineµ{ x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }µ denotes the
+The set \lstinlineµ{ x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }µ denotes the
 set of all integers between 0 and 9 and between 20 and 29.
 \end{example}
 \end{notimplementedenv}
@@ -422,7 +421,7 @@ Figure~\ref{fig:gram:assertions} summarizes grammar for assertions.
 \except{loop invariants lose their inductive nature}
 
 Figure~\ref{fig:gram:loops} shows grammar for loop annotations. There is no
-syntactic difference with \acsl. 
+syntactic difference with \acsl.
 \begin{figure}[htbp]
   \begin{cadre}
     \input{loops_modern.bnf}
@@ -453,7 +452,7 @@ In \eacsl, the same loop invariant $I$ is valid if and only if:
 \begin{itemize}
 \item $I$ holds before entering the loop; and
 \item if execution of the loop body in that state ends normally at the end of
-  the body or with a "continue" statement, $I$ is true in the resulting state. 
+  the body or with a "continue" statement, $I$ is true in the resulting state.
 \end{itemize}
 
 Thus the only difference with \acsl is that \eacsl does not assume that the
@@ -543,11 +542,9 @@ definition of its upper bound.
 \label{sec:statement_contract}
 \index{statement contract}\index{contract}
 
-\except{no \lstinline|abrupt| clauses}
+\nodiff
 
-Figure~\ref{fig:gram:contracts} shows grammar of statement contracts. Like
-function contracts, this is a simplified version of \acsl with no
-\lstinline|abrupt| clauses. All other constructs are unchanged.
+Figure~\ref{fig:gram:stcontracts} shows grammar of statement contracts.
 
 \begin{figure}[htbp]
   \begin{cadre}
@@ -706,7 +703,7 @@ predicates which are related to memory location.
 \nodiff
 
 \difficultswhy{\lstinline|\\base\_addr|,
-    \lstinline|\\block\_length|, \lstinline|\\valid|, 
+    \lstinline|\\block\_length|, \lstinline|\\valid|,
     \lstinline|\\valid_read| and
     \lstinline|\\offset|}{the implementation of a memory model}
 
@@ -723,9 +720,7 @@ predicates which are related to memory location.
 \subsection{Allocation and deallocation}
 \difficultswhy{All these constructs}{the implementation of a memory model}
 \label{sec:alloc-dealloc}
-
-\mywarning{this section is still almost experimental in \acsl. Thus it might still
-evolve in the future.}
+\nodiff
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -753,8 +748,21 @@ Figure~\ref{fig:gram:list} shows the notations for built-in lists.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\section{Abrupt termination}\label{sec:abrupt}
-\absentexperimental
+\section{\notimplemented{Abrupt termination}}
+\label{sec:abrupt}
+\index{abrupt termination}
+
+\nodiff
+
+Figure~\ref{fig:gram:abrupt} shows grammar of abrupt termination.
+
+\begin{figure}[htbp]
+  \begin{cadre}
+    \input{abrupt_modern.bnf}
+  \end{cadre}
+  \caption{Grammar of contracts about abrupt terminations}
+  \label{fig:gram:abrupt}
+\end{figure}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

@@ -2,9 +2,11 @@
   statement ::= "/*@" statement-contract "*/" statement
   \
   [ statement-contract ] ::= {("for" id ("," id)* ":")?} requires-clause* ;
-    simple-clause* named-behavior-stmt* ;
+    simple-clause-stmt* named-behavior-stmt* ;
     completeness-clause*
   \
+  simple-clause-stmt ::= simple-clause | { abrupt-clause-stmt }
+  \
   named-behavior-stmt ::= "behavior" id ":" behavior-body-stmt
   \
   behavior-body-stmt ::= assumes-clause* ;