Commit 9a3f7acd authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'bugfix/julien/update-refman' into 'stable/potassium'

Update E-ACSL reference manual

See merge request frama-c/e-acsl!293
parents b9e80f29 0334f63e
......@@ -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}
......@@ -117,6 +125,11 @@ in \lstinline|\\at|}
\section{Changes in \eacsl Implementation}
\subsection*{Version \eacslversion}
\begin{itemize}
\item \changeinsection{logicspec}{support of logic functions and predicates}
\end{itemize}
\subsection*{Version Argon-18}
\begin{itemize}
\item \changeinsection{at}{support of \lstinline|\\at| on purely
......
\begin{syntax}
C-global-decl ::= { "/*@" logic-def+ "*/" }
C-global-decl ::= "/*@" logic-def+ "*/"
\
[ { logic-def } ] ::= { logic-const-def } ;
| { logic-function-def } ;
| { logic-predicate-def } ;
logic-def ::= { logic-const-def } ;
| logic-function-def ;
| logic-predicate-def ;
\
[ { type-expr } ] ::= { id };
type-expr ::= id;
\
[ { logic-const-def } ] ::= { "logic" type-expr id "=" term ";" }
{ logic-const-def } ::= { "logic" type-expr id "=" term ";" }
\
[ { logic-function-def } ] ::= { "logic" type-expr id parameters "=" term ";" }
logic-function-def ::= "logic" type-expr id parameters "=" term ";"
\
[ { logic-predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
logic-predicate-def ::= "predicate" id parameters? "=" pred ";"
\
{ parameters } ::= { "(" parameter (, parameter)* ")" }
parameters ::= "(" parameter (, parameter)* ")"
\
{ parameter } ::= { type-expr id }
parameter ::= type-expr id
\end{syntax}
......@@ -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}
......
......@@ -612,7 +612,7 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{\notimplemented{Predicate and function definitions}}
\subsection{Predicate and function definitions}
\nodiff
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -642,7 +642,7 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{\notimplemented{Recursive logic definitions}}
\subsection{Recursive logic definitions}
\index{recursion}
\nodiff
......
Supports Markdown
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