diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex index 4f0069fb4e7c0d7e473ef5906dc90906f4b35de0..9e419b0fc1d84c7e97754ddf782071981b44aea8 100644 --- a/src/plugins/e-acsl/doc/refman/changes_modern.tex +++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex @@ -137,6 +137,8 @@ in \lstinline|\\at|} \item \changeinsection{reals}{support of rational numbers and operations} \item \changeinsection{fn-behavior}{remove abrupt clauses from the list of exceptions} +\item \changeinsection{fn-behavior}{support of \lstinline|complete behaviors| + and \lstinline|disjoint behaviors|} \item \changeinsection{statement_contract}{remove abrupt clauses from the list of exceptions} \item \changeinsection{abrupt}{add grammar for abrupt termination} diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex index cf6a3ebb9814ededf4a8f31d03341f3c099b2692..6db1b9dfa974cf8e773bb668896416f3de2f282f 100644 --- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex +++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex @@ -1,7 +1,7 @@ \begin{syntax} [ function-contract ] ::= requires-clause* { decreases-clause? } simple-clause* - named-behavior* { completeness-clause* } + named-behavior* completeness-clause* \ requires-clause ::= "requires" pred ";" \ @@ -24,6 +24,6 @@ \ assumes-clause ::= "assumes" pred ";" \ - { completeness-clause } ::= { "complete" "behaviors" (id (","id)*)? ";" } ; - | { "disjoint" "behaviors" (id (","id)*)? ";" } + completeness-clause ::= "complete" "behaviors" (id (","id)*)? ";" + | "disjoint" "behaviors" (id (","id)*)? ";" \end{syntax} diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex index 869c0d0e427e8504a1638ab7d97df20c439366a4..ef546063d84e099f17b5c1c8c101bcc4931f2042 100644 --- a/src/plugins/e-acsl/doc/refman/intro_modern.tex +++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex @@ -70,8 +70,7 @@ currently implemented into the \framac's \eacsl plug-in. & assigns \\ & allocates \\ & decreases \\ - & abrupt termination \\ - & complete and disjoint behaviors + & abrupt termination \\ \hline \end{tabular}