From e67c9730e85d9800bd05dcf8ac49de66d066f497 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 23 May 2019 17:26:15 +0200
Subject: [PATCH] update wrt upcoming version of ACSL

---
 src/plugins/e-acsl/doc/refman/assertions.tex     |  5 +++--
 src/plugins/e-acsl/doc/refman/changes_modern.tex | 10 +++++++++-
 src/plugins/e-acsl/doc/refman/main.tex           |  2 +-
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
index 0671104df07..cb6a92931a6 100644
--- a/src/plugins/e-acsl/doc/refman/assertions.tex
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -2,6 +2,7 @@
   C-compound-statement ::= "{" declaration* statement* assertion+ "}"
         \
   C-statement ::= assertion statement \
-  assertion ::= "/*@" "assert" pred ";" "*/" ;
-  | { "/*@" "for" id ("," id)* ":" "assert" pred ";" "*/" } ;
+  assertion-kind ::= "assert" | "check" \
+  assertion ::= "/*@" assertion-kind pred ";" "*/" ;
+  | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
 \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 b482e45965e..41f0774b869 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,14 @@
 
 \subsection*{Version \version}
 \begin{itemize}
+\item Update according to \acsl 1.14:
+  \begin{itemize}
+  \item \changeinsection{assertions}{add the keyword \texttt{check}}
+  \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.13}
+\begin{itemize}
 \item Update according to \acsl 1.13:
   \begin{itemize}
   \item \changeinsection{locations}{add syntax for set membership}
@@ -116,7 +124,7 @@ in \lstinline|\\at|}
     {
 \section{Changes in \eacsl Implementation}
 
-\subsection*{Version \eacslversion}
+\subsection*{Version Argon-18}
 
 \begin{itemize}
 \item \changeinsection{at}{support of \lstinline|\\at| on purely
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index e5704ebffee..88c2665b313 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -24,7 +24,7 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\acslversion}{1.13\xspace}
+\newcommand{\acslversion}{1.14\xspace}
 \newcommand{\version}{\acslversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
-- 
GitLab