From 0c9650036af08f7073e9ef5d2b24dcd793ff25fa Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 25 Mar 2021 15:41:04 +0100
Subject: [PATCH] [eacsl] Add support for "admit" in reference manual
---
src/plugins/e-acsl/doc/refman/changes_modern.tex | 1 +
src/plugins/e-acsl/doc/refman/fn_behavior.tex | 2 +-
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 4ee9e693bb0..1d0e08797a7 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 b97f9d8b982..8411919520d 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 ";"
\
--
GitLab