diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 3462abe5fba4c6afc3d5849146a89cdaa57b3037..282220d94f03967cea283f992fcbc0bc2415dd26 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/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 #
diff --git a/src/plugins/e-acsl/doc/refman/abrupt.tex b/src/plugins/e-acsl/doc/refman/abrupt.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5fe8ef4e9163b548cb9c423a5827345c7f19ac52
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/abrupt.tex
@@ -0,0 +1,15 @@
+\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}
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index ee30a79f7e0de4a4d9ae5f160c63fc98200dc495..70b99aa30c0b39a58eab38576cfd513ba65b3d60 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/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}
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index 4cd97341aa542521fb64da755d74617ab20726a5..cf6a3ebb9814ededf4a8f31d03341f3c099b2692 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -1,6 +1,6 @@
\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 ";" }
\
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index a3bcb11f398a544313ab5e90be3d9d61bfa4df6a..472b6cf40aaf229da2188f61a019941ba0d30cc3 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/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
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 88c2665b3138eb4593be41a543f86a070172ef12..8f53a75d66c09289d3f26f63fdef97dec50f452f 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/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,
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index c1482c0d65cbb0df19eccf95a887d310ac7a5f22..7c5b0e5a8fff1aeb7ff354be600d3398cf379045 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/refman/st_contracts.tex b/src/plugins/e-acsl/doc/refman/st_contracts.tex
index 498e9a73899ed7fd58fe49dfa210018d10d93964..8aefcbe9f322ac060e59ba1f56a97766fcff513f 100644
--- a/src/plugins/e-acsl/doc/refman/st_contracts.tex
+++ b/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* ;