diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex index 4ee9e693bb09b509bdd091077322d1fd66367d13..1d0e08797a7b049f152352f1e5de586ec34da129 100644 --- a/src/plugins/e-acsl/doc/refman/changes_modern.tex +++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex @@ -157,6 +157,7 @@ in \lstinline|\\at|} \begin{itemize} \item \changeinsection{expressions}{mark logic function and predicate applications as implemented} +\item \changeinsection{fn-behavior}{mark admit clauses as implemented} \end{itemize} \subsection*{Version Titanium-22} diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex index b97f9d8b9824ba0186852d130b9be6fa0a40fedd..8411919520dc7f488f79e41ada92b6b3899784f0 100644 --- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex +++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex @@ -3,7 +3,7 @@ { decreases-clause? } simple-clause* named-behavior* completeness-clause* \ - clause-kind ::= "check" | { "admit" } + clause-kind ::= "check" | "admit" \ requires-clause ::= clause-kind? "requires" pred ";" \