Commit 71073bba authored by Basile Desloges 's avatar Basile Desloges

[eacsl:doc] Update reference manual according to ACSL 1.16

parent 7fd007d6
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
C-compound-statement ::= "{" declaration* statement* assertion+ "}" C-compound-statement ::= "{" declaration* statement* assertion+ "}"
\ \
C-statement ::= assertion statement \ C-statement ::= assertion statement \
assertion-kind ::= "assert" | "check" \ assertion-kind ::= "assert" | clause-kind \
assertion ::= "/*@" assertion-kind pred ";" "*/" ; assertion ::= "/*@" assertion-kind pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ; | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
\end{syntax} \end{syntax}
...@@ -37,14 +37,14 @@ ...@@ -37,14 +37,14 @@
title = {{ACSL, ANSI/ISO C Specification Language}}, title = {{ACSL, ANSI/ISO C Specification Language}},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto}, Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
note = {Vesion 1.12. \url{http://frama-c.com/acsl.html}}, note = {\url{https://frama-c.com/html/acsl.html}},
} }
@manual{acslimplem, @manual{acslimplem,
title = {{ACSL version 1.12, Implementation in Silicon-20161101}}, title = {{ACSL, Implementation in Frama-C}},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto}, Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
note = {\url{http://frama-c.com/acsl.html}}, note = {\url{https://frama-c.com/download/frama-c-acsl-implementation.pdf}},
} }
@manual{framac, @manual{framac,
...@@ -52,20 +52,20 @@ ...@@ -52,20 +52,20 @@
author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
André Maroneze and André Maroneze and
Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski}, Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
note = {\url{http://frama-c.com}}, note = {\url{https://frama-c.com/download/frama-c-user-manual.pdf}},
} }
@manual{eacsl-plugin, @manual{eacsl-plugin,
title = {Frama-C's E-ACSL Plug-in}, title = {Frama-C's E-ACSL Plug-in},
author = {Julien Signoles and Kostyantyn Vorobyov}, author = {Julien Signoles and Kostyantyn Vorobyov},
note = {\url{http://frama-c.com/eacsl.html}}, note = {\url{https://frama-c.com/fc-plugins/e-acsl.html}},
} }
@manual{value, @manual{value,
title = {Frama-C's value analysis plug-in}, title = {Frama-C's Evolved Value Analysis analysis plug-in},
author = {Pascal Cuoq and Boris Yakobowski and Matthieu Lemerre and author = {Pascal Cuoq and Boris Yakobowski and Matthieu Lemerre and
André Maroneze and Valentin Perelle and Virgile Prevosto}, André Maroneze and Valentin Perelle and Virgile Prevosto},
note = {\url{http://frama-c.com/value.html}}, note = {\url{https://frama-c.com/fc-plugins/eva.html}},
} }
@book{KR88, @book{KR88,
......
\section{Changes} \section{Changes}
\subsection*{Version \version} \subsection*{Version \version}
\begin{itemize}
\item Update according to \acsl 1.16
\begin{itemize}
\item \changeinsection{fn-behavior}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\item \changeinsection{assertions}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\item \changeinsection{generalized-invariants}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\item \changeinsection{loop_annot}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\end{itemize}
\end{itemize}
\subsection*{Version 1.15}
\begin{itemize}
\item Update according to \acsl 1.15:
\begin{itemize}
\item \changeinsection{ghost}{add the \lstinline|\\ghost| qualifier}
\end{itemize}
\end{itemize}
\subsection*{Version 1.14}
\begin{itemize} \begin{itemize}
\item Update according to \acsl 1.14: \item Update according to \acsl 1.14:
\begin{itemize} \begin{itemize}
......
...@@ -3,7 +3,9 @@ ...@@ -3,7 +3,9 @@
{ decreases-clause? } simple-clause* { decreases-clause? } simple-clause*
named-behavior* completeness-clause* named-behavior* completeness-clause*
\ \
requires-clause ::= "requires" pred ";" clause-kind ::= "check" | { "admit" }
\
requires-clause ::= clause-kind? "requires" pred ";"
\ \
{ decreases-clause } ::= { "decreases" term ("for" id)? ";" } { decreases-clause } ::= { "decreases" term ("for" id)? ";" }
\ \
...@@ -16,7 +18,7 @@ ...@@ -16,7 +18,7 @@
\ \
{ location } ::= { tset } { location } ::= { tset }
\ \
ensures-clause ::= "ensures" pred ";" ensures-clause ::= clause-kind? "ensures" pred ";"
\ \
named-behavior ::= "behavior" id ":" behavior-body named-behavior ::= "behavior" id ":" behavior-body
\ \
......
\begin{syntax} \begin{syntax}
assertion ::= [ "/*@" "invariant" pred ";" "*/" ] ; assertion ::= [ "/*@" clause-kind? "invariant" pred ";" "*/" ] ;
| [ { "/*@" "for" id ("," id)* ":" "invariant" pred ";" "*/" } ] ; | [ { "/*@" "for" id ("," id)* ":" clause-kind? "invariant" pred ";" "*/" } ] ;
\end{syntax} \end{syntax}
\begin{syntax} \begin{syntax}
C-type-qualifier ::= C-type-qualifier ;
| { "\ghost" } ; only in ghost
\
ghost-type-specifier ::= C-type-specifier ; ghost-type-specifier ::= C-type-specifier ;
| { logic-type } \ | { logic-type } \
declaration ::= C-declaration ; declaration ::= C-declaration ;
...@@ -16,7 +19,8 @@ ...@@ -16,7 +19,8 @@
"(" C-argument-expression-list? ")"; "(" C-argument-expression-list? ")";
{"/*@" "ghost"} ; {"/*@" "ghost"} ;
{ "(" ghost-argument-expression-list ")"}; { "(" ghost-argument-expression-list ")"};
{ "*/"} ; call with ghosts { "*/"} ; call
; with ghosts
\ \
statement ::= C-statement ; statement ::= C-statement ;
| statements-ghost \ | statements-ghost \
......
...@@ -16,13 +16,13 @@ ...@@ -16,13 +16,13 @@
loop-clause ::= loop-invariant ; loop-clause ::= loop-invariant ;
| { loop-assigns } | { loop-assigns }
\ \
[ loop-invariant ] ::= [ "loop" "invariant" pred ";" ] ; [ loop-invariant ] ::= { clause-kind? } [ "loop" "invariant" pred ";" ] ;
\ \
{ loop-assigns } ::= { "loop" "assigns" locations ";" } ; { loop-assigns } ::= { "loop" "assigns" locations ";" } ;
\ \
{ loop-behavior } ::= { "for" id ("," id)* ":" } ; { loop-behavior } ::= { "for" id ("," id)* ":" } ;
{ loop-clause* } ; \hspace{-30mm} annotation for behavior $id$ { loop-clause* } ; \hspace{-35mm} annotation for behavior $id$
\ \
{ loop-variant } ::= { "loop" "variant" term ";" } ; { loop-variant } ::= { "loop" "variant" term ";" } ;
| { "loop" "variant" term "for" id ";" } ; \hspace{-30mm} variant for relation $id$ | { "loop" "variant" term "for" id ";" } ; \hspace{-35mm} variant for relation $id$
\end{syntax} \end{syntax}
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
\usepackage{alltt} \usepackage{alltt}
\makeindex \makeindex
\newcommand{\eacsllangversion}{1.14\xspace} \newcommand{\eacsllangversion}{1.16\xspace}
\newcommand{\version}{\eacsllangversion\xspace} \newcommand{\version}{\eacsllangversion\xspace}
\renewcommand{\textfraction}{0.01} \renewcommand{\textfraction}{0.01}
......
...@@ -290,11 +290,6 @@ It is not possible to define logic types introduced by the specification writer ...@@ -290,11 +290,6 @@ It is not possible to define logic types introduced by the specification writer
\eacsl plug-in. \eacsl plug-in.
\end{notimplementedenv} \end{notimplementedenv}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{String literals}
\nodiff
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
...@@ -385,7 +380,7 @@ set of all integers between 0 and 9 and between 20 and 29. ...@@ -385,7 +380,7 @@ set of all integers between 0 and 9 and between 20 and 29.
\begin{notimplementedenv} \begin{notimplementedenv}
Ranges are currently only supported in memory built-ins described in Ranges are currently only supported in memory built-ins described in
Section~\ref{subsec:memory} and~\ref{sec:dangling}. Section~\ref{subsec:memory},~\ref{sec:initialized} and~\ref{sec:dangling}.
\begin{example} \begin{example}
The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that
...@@ -484,6 +479,7 @@ loop invariants are not inductive. ...@@ -484,6 +479,7 @@ loop invariants are not inductive.
\end{example} \end{example}
\subsubsection{General inductive invariant} \subsubsection{General inductive invariant}
\label{sec:generalized-invariants}
Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants} Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
\begin{figure}[t] \begin{figure}[t]
...@@ -725,7 +721,7 @@ predicates which are related to memory location. ...@@ -725,7 +721,7 @@ predicates which are related to memory location.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Allocation and deallocation} \subsection{Dynamic allocation and deallocation}
\difficultswhy{All these constructs}{the implementation of a memory model} \difficultswhy{All these constructs}{the implementation of a memory model}
\label{sec:alloc-dealloc} \label{sec:alloc-dealloc}
\nodiff \nodiff
...@@ -852,13 +848,18 @@ same than the one of \acsl. ...@@ -852,13 +848,18 @@ same than the one of \acsl.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Undefined values, dangling pointers} \section{Initialization and undefined values}
\label{sec:initialized}
\nodiff
\difficultwhy{\lstinline|\\initialized|}{the implementation of a memory model}
\section{Dangling pointers}
\label{sec:dangling} \label{sec:dangling}
\nodiff \nodiff
\difficultswhy{\lstinline|\\initialized| and \difficultwhy{\notimplemented{\lstinline|\\dangling|}}{the implementation of a
\notimplemented{\lstinline|\\dangling|}}{the implementation of a memory memory model}
model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
...@@ -867,3 +868,17 @@ same than the one of \acsl. ...@@ -867,3 +868,17 @@ same than the one of \acsl.
\section{Well-typed pointers} \section{Well-typed pointers}
\label{sec:typedpointers} \label{sec:typedpointers}
\absentexperimental \absentexperimental
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Logic attribute annotations}
\absentexperimental
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Preprocessing for ACSL}
\nodiff
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