From 71073bbab82751a5559cc656b70e8c17c30e83eb Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 16 Nov 2020 18:15:20 +0100
Subject: [PATCH] [eacsl:doc] Update reference manual according to ACSL 1.16
---
src/plugins/e-acsl/doc/refman/assertions.tex | 2 +-
src/plugins/e-acsl/doc/refman/biblio.bib | 14 +++----
.../e-acsl/doc/refman/changes_modern.tex | 23 ++++++++++++
src/plugins/e-acsl/doc/refman/fn_behavior.tex | 6 ++-
.../e-acsl/doc/refman/generalinvariants.tex | 4 +-
src/plugins/e-acsl/doc/refman/ghost.tex | 6 ++-
src/plugins/e-acsl/doc/refman/loops.tex | 6 +--
src/plugins/e-acsl/doc/refman/main.tex | 2 +-
.../e-acsl/doc/refman/speclang_modern.tex | 37 +++++++++++++------
9 files changed, 72 insertions(+), 28 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
index cb6a92931a6..9758d44bec6 100644
--- a/src/plugins/e-acsl/doc/refman/assertions.tex
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -2,7 +2,7 @@
C-compound-statement ::= "{" declaration* statement* assertion+ "}"
\
C-statement ::= assertion statement \
- assertion-kind ::= "assert" | "check" \
+ assertion-kind ::= "assert" | clause-kind \
assertion ::= "/*@" assertion-kind pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/biblio.bib b/src/plugins/e-acsl/doc/refman/biblio.bib
index 15823978c98..bb7f2f66e7f 100644
--- a/src/plugins/e-acsl/doc/refman/biblio.bib
+++ b/src/plugins/e-acsl/doc/refman/biblio.bib
@@ -37,14 +37,14 @@
title = {{ACSL, ANSI/ISO C Specification Language}},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
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,
- 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
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,
@@ -52,20 +52,20 @@
author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
André Maroneze and
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,
title = {Frama-C's E-ACSL Plug-in},
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,
- 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
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,
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 9e419b0fc1d..5399a380510 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -1,6 +1,29 @@
\section{Changes}
\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}
\item Update according to \acsl 1.14:
\begin{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index 6db1b9dfa97..b97f9d8b982 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -3,7 +3,9 @@
{ decreases-clause? } simple-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)? ";" }
\
@@ -16,7 +18,7 @@
\
{ location } ::= { tset }
\
- ensures-clause ::= "ensures" pred ";"
+ ensures-clause ::= clause-kind? "ensures" pred ";"
\
named-behavior ::= "behavior" id ":" behavior-body
\
diff --git a/src/plugins/e-acsl/doc/refman/generalinvariants.tex b/src/plugins/e-acsl/doc/refman/generalinvariants.tex
index 246a377d67f..f72665035ec 100644
--- a/src/plugins/e-acsl/doc/refman/generalinvariants.tex
+++ b/src/plugins/e-acsl/doc/refman/generalinvariants.tex
@@ -1,4 +1,4 @@
\begin{syntax}
- assertion ::= [ "/*@" "invariant" pred ";" "*/" ] ;
- | [ { "/*@" "for" id ("," id)* ":" "invariant" pred ";" "*/" } ] ;
+ assertion ::= [ "/*@" clause-kind? "invariant" pred ";" "*/" ] ;
+ | [ { "/*@" "for" id ("," id)* ":" clause-kind? "invariant" pred ";" "*/" } ] ;
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/ghost.tex b/src/plugins/e-acsl/doc/refman/ghost.tex
index 1d6d0e9c9e6..6d5cefc68a1 100644
--- a/src/plugins/e-acsl/doc/refman/ghost.tex
+++ b/src/plugins/e-acsl/doc/refman/ghost.tex
@@ -1,5 +1,8 @@
\begin{syntax}
+ C-type-qualifier ::= C-type-qualifier ;
+ | { "\ghost" } ; only in ghost
+ \
ghost-type-specifier ::= C-type-specifier ;
| { logic-type } \
declaration ::= C-declaration ;
@@ -16,7 +19,8 @@
"(" C-argument-expression-list? ")";
{"/*@" "ghost"} ;
{ "(" ghost-argument-expression-list ")"};
- { "*/"} ; call with ghosts
+ { "*/"} ; call
+ ; with ghosts
\
statement ::= C-statement ;
| statements-ghost \
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 5d1fa33003c..1de09ce3a63 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -16,13 +16,13 @@
loop-clause ::= loop-invariant ;
| { loop-assigns }
\
- [ loop-invariant ] ::= [ "loop" "invariant" pred ";" ] ;
+ [ loop-invariant ] ::= { clause-kind? } [ "loop" "invariant" pred ";" ] ;
\
{ loop-assigns } ::= { "loop" "assigns" locations ";" } ;
\
{ 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" term "for" id ";" } ; \hspace{-30mm} variant for relation $id$
+ | { "loop" "variant" term "for" id ";" } ; \hspace{-35mm} variant for relation $id$
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 4b6ad34ce83..f64b135dd8f 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{\eacsllangversion}{1.14\xspace}
+\newcommand{\eacsllangversion}{1.16\xspace}
\newcommand{\version}{\eacsllangversion\xspace}
\renewcommand{\textfraction}{0.01}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 261843a3906..a15c8384b4a 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -290,11 +290,6 @@ It is not possible to define logic types introduced by the specification writer
\eacsl plug-in.
\end{notimplementedenv}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\subsection{String literals}
-\nodiff
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -385,7 +380,7 @@ set of all integers between 0 and 9 and between 20 and 29.
\begin{notimplementedenv}
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}
The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that
@@ -484,6 +479,7 @@ loop invariants are not inductive.
\end{example}
\subsubsection{General inductive invariant}
+\label{sec:generalized-invariants}
Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
\begin{figure}[t]
@@ -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}
\label{sec:alloc-dealloc}
\nodiff
@@ -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}
\nodiff
-\difficultswhy{\lstinline|\\initialized| and
- \notimplemented{\lstinline|\\dangling|}}{the implementation of a memory
- model}
+\difficultwhy{\notimplemented{\lstinline|\\dangling|}}{the implementation of a
+ memory model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -867,3 +868,17 @@ same than the one of \acsl.
\section{Well-typed pointers}
\label{sec:typedpointers}
\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Logic attribute annotations}
+\absentexperimental
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Preprocessing for ACSL}
+\nodiff
--
GitLab