diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex index 0671104df075c2dd60049795472441e5e0776620..cb6a92931a6f11881d2ebff24922c092a30b9a95 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 b482e45965e933015939a0b2f318fa8ac4b1e1af..41f0774b869be9a3bf10e9903b8e151fafe97bf8 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 e5704ebffeed9b32e2583f4df27ddfa69066f672..88c2665b3138eb4593be41a543f86a070172ef12 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}