Commit e67c9730 authored by Julien Signoles's avatar Julien Signoles
Browse files

update wrt upcoming version of ACSL

parent 992147e7
......@@ -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}
......@@ -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
......
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment