From 88e296f4654329993c9292af3fdd55bfded00473 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 16 Dec 2020 10:34:59 +0100
Subject: [PATCH] [e-acsl:refman] mark logic function and predicate
applications as implemented
---
src/plugins/e-acsl/doc/refman/changes_modern.tex | 6 +++++-
src/plugins/e-acsl/doc/refman/predicate.tex | 2 +-
src/plugins/e-acsl/doc/refman/term.tex | 2 +-
3 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 44fd0956cf0..63741120077 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -151,7 +151,11 @@ in \lstinline|\\at|}
\section{Changes in \eacsl Implementation}
% Next version
-%\subsection*{Version \eacslplugincodename-\eacslpluginversion}
+\subsection*{Version \eacslplugincodename-\eacslpluginversion}
+\begin{itemize}
+\item \changeinsection{expressions}{mark logic function and predicate
+ applications as implemented}
+\end{itemize}
\subsection*{Version Titanium-22}
diff --git a/src/plugins/e-acsl/doc/refman/predicate.tex b/src/plugins/e-acsl/doc/refman/predicate.tex
index ae1dcfb6108..c89a1ed2979 100644
--- a/src/plugins/e-acsl/doc/refman/predicate.tex
+++ b/src/plugins/e-acsl/doc/refman/predicate.tex
@@ -3,7 +3,7 @@
\
pred ::= "\true" | "\false" ;
| term (rel-op term)+ ; comparisons
- | { id "(" term ("," term)* ")" } ; predicate application
+ | id "(" term ("," term)* ")" ; predicate application
| "(" pred ")" ; parentheses
| [ pred "&&" pred ] ; conjunction
| [ pred "||" pred ] ; disjunction
diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex
index 0582703adc5..67e3edea785 100644
--- a/src/plugins/e-acsl/doc/refman/term.tex
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -26,7 +26,7 @@
| { "{" term "\with" "."id "=" term "}" } ; field functional modifier
| term "->" id ;
| [ "(" type-expr ")" term ] ; cast
- | { id "(" term ("," term)* ")" } ; function application
+ | id "(" term ("," term)* ")" ; function application
| "(" term ")" ; parentheses
| [ term "?" term ":" term ] ; ternary condition
| "\let" id "=" term ";" term ; local binding
--
GitLab