diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index c71c70b01f0fbbc9d34312330f1a015a144a3c29..4814aa3de68bdd6d17d32d595cee401abb95bd43 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -17,7 +17,11 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
assertions_modern.bnf loops_modern.bnf st_contracts_modern.bnf \
logic_modern.bnf data_invariants_modern.bnf model_modern.bnf \
ghost_modern.bnf generalinvariants_modern.bnf iterator_modern.bnf \
- abrupt_modern.bnf bsearch.c bsearch2.c link.c
+ guarded_quantif_modern.bnf inductive_modern.bnf logicdecl_modern.bnf \
+ higherorder_modern.bnf logictypedecl_modern.bnf logicreads_modern.bnf \
+ allocation_modern.bnf abrupt_modern.bnf dependencies_modern.bnf \
+ volatile-gram_modern.bnf \
+ bsearch.c bsearch2.c link.c
##############
# Main rules #
diff --git a/src/plugins/e-acsl/doc/refman/abrupt.tex b/src/plugins/e-acsl/doc/refman/abrupt.tex
index 5fe8ef4e9163b548cb9c423a5827345c7f19ac52..06ba5a62a92fdcebf74d5fc619a44f34566e727f 100644
--- a/src/plugins/e-acsl/doc/refman/abrupt.tex
+++ b/src/plugins/e-acsl/doc/refman/abrupt.tex
@@ -3,7 +3,9 @@
\
{ exits-clause } ::= { "exits" pred ";" }
\
- { abrupt-clause-stmt } ::= { breaks-clause } | { continues-clause } | { returns-clause }
+ { abrupt-clause-stmt } ::= { breaks-clause } | { continues-clause } |
+ { returns-clause } ;
+ { exits-clause }
\
{ breaks-clause } ::= { "breaks" pred ";" }
\
diff --git a/src/plugins/e-acsl/doc/refman/allocation.tex b/src/plugins/e-acsl/doc/refman/allocation.tex
new file mode 100644
index 0000000000000000000000000000000000000000..2d9a018faec68af1505aa5d27d524eb33b58c070
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/allocation.tex
@@ -0,0 +1,9 @@
+\begin{syntax}
+ { allocation-clause } ::= { "allocates" dyn-allocation-addresses ";" } ;
+ | { "frees" dyn-allocation-addresses ";" } ;
+ \
+ { loop-allocation } ::= { "loop" "allocates" dyn-allocation-addresses ";" };
+ | { "loop" "frees" dyn-allocation-addresses ";" };
+ \
+ { dyn-allocation-addresses } ::= { locations } ;
+ \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
index 9758d44bec67f2d6e22fe5c76d87e16ef81ce862..334b7d1869a81ac692beab8b102847606b1bd3ed 100644
--- a/src/plugins/e-acsl/doc/refman/assertions.tex
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -1,8 +1,17 @@
\begin{syntax}
- C-compound-statement ::= "{" declaration* statement* assertion+ "}"
- \
- C-statement ::= assertion statement \
- assertion-kind ::= "assert" | clause-kind \
- assertion ::= "/*@" assertion-kind pred ";" "*/" ;
- | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
+ C-compound-statement ::=
+ "{" C-declaration* ;
+ C-statement* assertion+ "}"
+ \
+ C-statement ::= assertion ;
+ C-statement
+ \
+ assertion-kind ::= "assert" ; assertion
+ | clause-kind ; non-blocking assertion
+ \
+ assertion ::= "/*@" assertion-kind pred";" ;
+ "*/" ;
+ | { "/*@" "for" id ("," id)*":" } ;
+ { assertion-kind pred";" };
+ { "*/" }
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
index 88bbc974a191e189a3fdaa7e88047b65abf6387f..5612fcc672bf818bf0475f81c85162a5feae1991 100644
--- a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
@@ -1,12 +1,18 @@
main(void) {
int m = 2;
int n = 7;;
- K: ;
- n = 875;
+ L1: ;
+ n = 4;
+ L2:
/*@ assert
- \let k = 3;
+ \let k = m + 1;
\exists integer u; 9 <= u < 21 &&
\forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
\at(n + u + v > 0, K); */ ;
+ /*@ assert
+ \let k = m + 1;
+ \exists integer u; n <= u < 21 && // [u] depends on [n]
+ \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
+ \at(n + u + v > 0, L1); */ ;
return 0;
}
diff --git a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
index dff4da97bd3e5b3fa986023c89a94a7307563cd5..a326f66b45287545f2a92c342f4344ff9b878e5f 100644
--- a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
@@ -1,2 +1,2 @@
/*@ ensures \forall int i; 0 <= i < n-1 ==> \old(t[i]) == t[i+1]; */
-void reverse(int *t, int n) { }
+void reverse(int *t, int n);
diff --git a/src/plugins/e-acsl/doc/refman/biblio.bib b/src/plugins/e-acsl/doc/refman/biblio.bib
index da3c4fc29c6344593301fb20559623872f7eb71a..1d9bf947468fc85f4b1d9361df107d38e45356b9 100644
--- a/src/plugins/e-acsl/doc/refman/biblio.bib
+++ b/src/plugins/e-acsl/doc/refman/biblio.bib
@@ -61,13 +61,21 @@ Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
note = {\url{https://frama-c.com/fc-plugins/e-acsl.html}},
}
-@manual{value,
- 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},
+@manual{eva,
+ title = {Eva --- The Evolved Value Analysis Plug-in},
+ author = {David B\"uhler and Pascal Cuoq and Boris Yakobowski and
+ Matthieu Lemerre and André Maroneze and Valentin Perelle and
+ Virgile Prevosto},
note = {\url{https://frama-c.com/fc-plugins/eva.html}},
}
+@manual{wp,
+ title = {Wp Plug-in Manual},
+ author = {Patrick Baudin and François Bobot and Lo\"ic Correnson and
+ Zaynah Dargaye and Allan Blanchard},
+ note = {\url{https://frama-c.com/fc-plugins/wp.html}},
+}
+
@book{KR88,
author = {Brian Kernighan and Dennis Ritchie},
title = {The C Programming Language (2nd Ed.)},
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 1d0e08797a7b049f152352f1e5de586ec34da129..b37bb6f30daa112897e172fdfc5e023daf355a2b 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -1,7 +1,28 @@
\section{Changes}
% Next version
-%\subsection*{Version \version}
+\subsection*{Version \version}
+
+\begin{itemize}
+ \item \changeinsection{expressions}{xor \lstinline|\^\^| is not lazy}
+ \item \changeinsection{expressions}{new extended syntax for quantifications}
+ \item \changeinsection{reals}{additional remark about real numbers and
+ operations over them}
+ \item \changeinsection{locations}{new extended syntax for set comprehensions}
+ \item \changeinsection{at}{more restrictive scoping rule for \lstinline|\\at|
+ constructs.}
+ \item \changeinsection{logicspec}{add lemmas and data invariants}
+ \item \changeinsection{inductivepredicates}{add inductive predicates
+ experimentally: the accepted subset will be refined in a future version}
+ \item \changeinsection{axiomatic}{add axiomatic declarations
+ experimentally: the accepted subset will be refined in a future version}
+ \item \changeinsection{polym-logic-types}{add polymorphic logic types}
+ \item \changeinsection{higherorder}{add higher-order logic constructions}
+ \item \changeinsection{concrete-logic-types}{add concrete logic types}
+ \item \changeinsection{reads}{add \lstinline|read| clauses}
+ \item \changeinsection{func-dep}{add dependencies information}
+ \item \changeinsection{volatile-variables}{add volatile constructs}
+\end{itemize}
\subsection*{Version 1.16}
\begin{itemize}
@@ -157,7 +178,8 @@ in \lstinline|\\at|}
\begin{itemize}
\item \changeinsection{expressions}{mark logic function and predicate
applications as implemented}
-\item \changeinsection{fn-behavior}{mark admit clauses as implemented}
+\item \changeinsection{fn-behavior}{mark admit and check clauses as implemented}
+\item \changeinsection{loop_annot}{mark loop variants as implemented}
\end{itemize}
\subsection*{Version Titanium-22}
diff --git a/src/plugins/e-acsl/doc/refman/concl_modern.tex b/src/plugins/e-acsl/doc/refman/concl_modern.tex
index 58ce943e29c189fb4d75b0098c5683e6405c834c..816d8ca068b939f9d519bdcb9b628c82324e9e49 100644
--- a/src/plugins/e-acsl/doc/refman/concl_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/concl_modern.tex
@@ -4,6 +4,6 @@
This document presents an Executable ANSI/ISO C Specification Language. It
provides a subset of \acsl~\cite{acsl} implemented~\cite{acslimplem} in the
\framac platform~\cite{framac} in which each construct may be evaluated at
-runtime. The specification language described here is intented to evolve in the
+runtime. The specification language described here is intended to evolve in the
future in two directions. First it is based on \acsl which is itself still
evolving. Second the considered subset of \acsl may also change.
diff --git a/src/plugins/e-acsl/doc/refman/data_invariants.tex b/src/plugins/e-acsl/doc/refman/data_invariants.tex
index 6f9186f8c441db2ab04add58868491d60660b32b..f8cc14bdda39b1be98f3dc39854671386b82dd82 100644
--- a/src/plugins/e-acsl/doc/refman/data_invariants.tex
+++ b/src/plugins/e-acsl/doc/refman/data_invariants.tex
@@ -1,7 +1,5 @@
\begin{syntax}
- declaration ::= { "/*@" data-inv-decl "*/" }
- \
- { data-inv-decl } ::= { data-invariant } | { type-invariant }
+ { data-inv-def } ::= { data-invariant } | { type-invariant }
\
{ data-invariant } ::= { { inv-strength? } "global" "invariant" } ;
{ id ":" pred ";" }
diff --git a/src/plugins/e-acsl/doc/refman/dependencies.tex b/src/plugins/e-acsl/doc/refman/dependencies.tex
new file mode 100644
index 0000000000000000000000000000000000000000..0a385457c228d1868d242f05767edc29406f576c
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/dependencies.tex
@@ -0,0 +1,4 @@
+\begin{syntax}
+{ assigns-clause } ::= { "assigns" locations-list ("\from" locations )? ";" } ;
+ | { "assigns" term "\from" locations "=" term ";" }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index 3831ef9c22aec5acbc7fdcb964f88ff21eb95815..9a95f8b493cc803df8d75067cf1ef3e1472ce733 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -7,14 +7,16 @@
\
requires-clause ::= clause-kind? "requires" pred ";"
\
- { decreases-clause } ::= { "decreases" term ("for" id)? ";" }
+ { decreases-clause } ::= { "decreases" term ("for" ident)? ";" }
\
- [ simple-clause ] ::= { assigns-clause } | ensures-clause ;
- | { allocation-clause} | { abrupt-clause }
+ simple-clause ::= { assigns-clause } | ensures-clause ;
+ | { allocation-clause} | { abrupt-clause }
\
{ assigns-clause } ::= { "assigns" locations ";" }
\
- { locations } ::= { location ("," location) * | "\nothing" }
+ { locations } ::= { locations-list | "\nothing" }
+ \
+ { locations-list } ::= { location ("," location) * }
\
{ location } ::= { tset }
\
diff --git a/src/plugins/e-acsl/doc/refman/ghost.tex b/src/plugins/e-acsl/doc/refman/ghost.tex
index 6d5cefc68a1abf69dad33a52b5270d8cd7e782cc..1766ea6afa0e077cd5d4727d9ea3ea6477529484 100644
--- a/src/plugins/e-acsl/doc/refman/ghost.tex
+++ b/src/plugins/e-acsl/doc/refman/ghost.tex
@@ -1,40 +1,39 @@
\begin{syntax}
- C-type-qualifier ::= C-type-qualifier ;
- | { "\ghost" } ; only in ghost
+ C-type-qualifier ::= { "\ghost" } ; only in ghost
\
- ghost-type-specifier ::= C-type-specifier ;
- | { logic-type } \
- declaration ::= C-declaration ;
- | "/*@" "ghost" ghost-declaration "*/" \
- direct-declarator ::= C-direct-declarator ;
- | direct-declarator ;
- "(" C-parameter-type-list? ")";
- {"/*@" "ghost"};
- {"("ghost-parameter-list")"};
- {"*/"}; ghost args
- \
- postfix-expression ::= C-postfix-expression ;
- | postfix-expression ;
- "(" C-argument-expression-list? ")";
- {"/*@" "ghost"} ;
- { "(" ghost-argument-expression-list ")"};
- { "*/"} ; call
- ; with ghosts
- \
- statement ::= C-statement ;
- | statements-ghost \
- statements-ghost ::= "/*@" "ghost" ;
- ghost-statement+ "*/" \
- ghost-selection-statement ::= C-selection-statement ;
+ C-type-specifier ::= { logic-type }
+ \
+ logic-def ::= "ghost" C-declaration ;
+ \
+ C-direct-declarator ::=
+ C-direct-declarator ; function declarator
+ "(" C-parameter-type-list? ;
+ ")" "/*@" "ghost" "(" ;
+ C-parameter-type-list; with ghost params
+ ")" "*/";
+ \
+ C-postfix-expression ::=
+ C-postfix-expression ; function call
+ "(" C-argument-expression-list? ;
+ ")" "/*@" "ghost" "(" ;
+ C-argument-expression-list; with ghost args
+ ")";
+ "*/" ;
+ \
+ C-statement ::=
+ "/*@" "ghost";
+ C-statement+ ; ghost code
+ "*/" ;
| "if" "(" C-expression ")";
statement;
- {"/*@" "ghost" "else"};
- { ghost-statement+ };
- { "*/"} \
-
- struct-declaration ::= C-struct-declaration ;
- | {"/*@" "ghost" };
- {struct-declaration "*/"} ; ghost field
-
+ "/*@" "ghost" ;
+ "else" C-statement ; ghost alternative
+ C-statement* ; unconditional ghost code
+ "*/"
+ \
+ C-struct-declaration ::=
+ {"/*@" "ghost" };
+ {C-struct-declaration} ; ghost field
+ {"*/"}
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/guarded_quantif.tex b/src/plugins/e-acsl/doc/refman/guarded_quantif.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5edd7c86f13453718e6c19fa2969d8134cd93d99
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/guarded_quantif.tex
@@ -0,0 +1,10 @@
+\begin{syntax}
+ guarded-quantif ::= "\forall" binders ";" (guards "==>")+ pred ;
+ | "\exists" binders ";" guards "&&" pred ;
+ \
+ guards ::= interv ("&&" interv)* ;
+ \
+ interv ::= term (guard-op id)+ guard-op term ;
+ \
+ guard-op ::= "<=" | "<" ;
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/higherorder.tex b/src/plugins/e-acsl/doc/refman/higherorder.tex
new file mode 100644
index 0000000000000000000000000000000000000000..cc4d91104bc4afbbbb6d7307695adc33347bf5c6
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/higherorder.tex
@@ -0,0 +1,8 @@
+\begin{syntax}
+term ::= { "\lambda" binders ";" term } ; abstraction
+| { ext-quantifier "(" term "," term "," term ")" };
+| { "{" term "\with" "[" range "]" "=" term "}" } ;
+\
+{ ext-quantifier } ::= { "\max" } | { "\min" } | { "\sum" };
+ | { "\product" } | { "\numof" }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/inductive.tex b/src/plugins/e-acsl/doc/refman/inductive.tex
new file mode 100644
index 0000000000000000000000000000000000000000..f3eac0905ac2b71df7013afd37949f0ab91d3896
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/inductive.tex
@@ -0,0 +1,8 @@
+\begin{syntax}
+ logic-def ::= { inductive-def }
+ \
+ { inductive-def } ::= { "inductive" } ;
+ { poly-id parameters? "{" indcase* "}" }
+ \
+ { indcase } ::= { "case" poly-id ":" pred ";" }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index 4e85af395ced1a11e8513c64f3c13fb55cca4d32..328721a32e7a6568edcf86cbe73b61207b560940 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -8,9 +8,8 @@ This document is a reference manual for
{E-ACSL.}
\eacsl is an acronym for ``Executable ANSI/ISO C
Specification Language''. It is an ``executable'' subset of
-\emph{stable} \acsl~\cite{acsl} implemented~\cite{acslimplem} in the \framac
-platform~\cite{framac}. ``Stable'' means that no experimental \acsl feature is
-supported by \eacsl. Contrary to \acsl, each \eacsl specification is
+\acsl~\cite{acsl} implemented~\cite{acslimplem} in the \framac
+platform~\cite{framac}. Contrary to \acsl, each \eacsl specification is
executable: it may be evaluated at runtime.
In this document, we assume that the reader has a good knowledge of both
@@ -47,28 +46,53 @@ currently implemented into the \framac's \eacsl plug-in.
& mathematical reals \\
\hline
terms
- & \lstinline|\\true| and \lstinline|\\false| \\
- & let binding \\
+ & truth values \lstinline|\\true| and \lstinline|\\false| \\
+ & functional updates \\
+ & irrational numbers \\
+ & built-in function \lstinline|\\length| over arrays \\
+ & conversions of structure to structure \\
& t-sets \\
+ & higher-order logic constructs \\
+ & hybrid functions \\
+ & labeled memory-related built-in functions \\
+ & finite sets \\
+ & finite lists \\
+ & \lstinline|\\exit_status|
+ \\
\hline
predicates
- & exclusive or operator \\ % \lstinline|^^|
- & let bindings \\
- & quantifications over non-integer types \\
- & \lstinline|\\specified|
+ & let bindings of predicates \\
+ & unguarded quantifications over small types \\
+ & quantifications over pointers and enums \\
+ & iterators \\
+ & comparisons of unions and structures \\
+ & t-sets \\
+ & hybrid predicates \\
+ & labeled memory-related built-in predicates \\
+ & dangling pointers \lstinline|\\dangling|
\\
\hline
- annotations
- & behavior-specific annotations \\
- & loop assigns \\
- & global annotations
+ clauses
+ & decreases clauses \\
+ & assigns clauses \\
+ & allocation and deallocation clauses \\
+ & abrupt clauses \\
+ & reads clauses
\\
\hline
- behavior clauses
- & assigns \\
- & allocates \\
- & decreases \\
- & abrupt termination
+ annotations
+ & behavior-specific annotations (introduced by \lstinline|for|) \\
+ & loop assigns \\
+ & loop allocations \\
+ & lemmas \\
+ & inductive predicates \\
+ & axiomatic definitions \\
+ & polymorphic logic types \\
+ & concrete logic types \\
+ & specification modules \\
+ & data invariants \\
+ & model variables and model fields \\
+ & volatile variables
\\
\hline
\end{tabular}
diff --git a/src/plugins/e-acsl/doc/refman/iterator.tex b/src/plugins/e-acsl/doc/refman/iterator.tex
index 156f6df939a182541e1b808cb176bcbfbc68778f..9c7802b98fe164490b9b59650aff0aa955ae909e 100644
--- a/src/plugins/e-acsl/doc/refman/iterator.tex
+++ b/src/plugins/e-acsl/doc/refman/iterator.tex
@@ -1,12 +1,17 @@
\begin{syntax}
- declaration ::= [ { "//@" "iterator" id "("wildcard-param","
+ [ { iterator } ] ::= [ { "\forall" binders ";" iterator-guard "==>" pred } ];
+ | [ { "\exists" binders ";" iterator-guard "&&" pred } ] ;
+ \
+ [ { iterator-guard } ] ::= [ { id"("term"," term")" } ]
+ \
+ [ { declaration } ] ::= [ { "//@" "iterator" id "("wildcard-param","
wildcard-param")" ":" } ] ;
[ { "nexts" terms ";" "guards" predicates ";" } ]
\
[ { wildcard-param } ] ::= { parameter } ;
| [ { "_" } ]
\
- [ { terms } ] ::= [ { term (, term)* } ]
+ { terms } ::= { term (, term)* }
\
- [ { predicates } ] ::= [ { predicate (, predicate)* } ]
+ { predicates } ::= { predicate (, predicate)* }
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/list-gram.tex b/src/plugins/e-acsl/doc/refman/list-gram.tex
index de081932cead22daf4ba87f59ca580258a1fff98..ec2be483c44bbb4a0c88240379a86201187d4580 100644
--- a/src/plugins/e-acsl/doc/refman/list-gram.tex
+++ b/src/plugins/e-acsl/doc/refman/list-gram.tex
@@ -1,7 +1,7 @@
\begin{syntax}
- term ::= "[|" "|]" ; empty list
- | "[|" term ("," term)* "|]" ; list of elements
- | term "^" term ; list concatenation (overloading bitwise-xor
+ term ::= { "[|" "|]" } ; empty list
+ | { "[|" term ("," term)* "|]" } ; list of elements
+ | { term "^" term } ; list concatenation (overloading bitwise-xor
; operator)
- | term "*^" term ; list repetition
+ | { term "*^" term } ; list repetition
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/loc.tex b/src/plugins/e-acsl/doc/refman/loc.tex
index 37cdb3a22a20114794fe130e719b86daf86e6222..a360c1f75fd35ec79560ecd82e23933c0b862e79 100644
--- a/src/plugins/e-acsl/doc/refman/loc.tex
+++ b/src/plugins/e-acsl/doc/refman/loc.tex
@@ -1,21 +1,24 @@
\begin{syntax}
- tset ::= { "\empty" } ; empty set
- | tset "->" id ;
- | tset "." id ;
- | "*" tset ;
- | "&" tset ;
- | tset "[" tset "]" ;
- | [ term ".." term ] ; range
- | { "\union" "(" tset ("," tset)* ")" } ; union of locations
- | { "\inter" "(" tset ("," tset)* ")" }; intersection
+ [ range ] ::= [ term ".." term ] ;
+ \
+ [ tset ] ::= { "\empty" } ; empty set
+ | { tset "->" id } ;
+ | { tset "." id } ;
+ | { "*" tset } ;
+ | { "&" tset } ;
+ | { tset "[" tset "]" } ;
+ | { tset "[" range "]" } ;
+ | "(" range ")" ; a range as a set of integers
+ | { "\union" "(" tset ("," tset)* ")" } ; union of location sets
+ | { "\inter" "(" tset ("," tset)* ")" } ; intersection of location sets
| tset "+" tset ;
| "(" tset ")" ;
- | {[the given term cannot itself be a set]
- "{" tset "|" binders (";" pred)? "}"} ; set comprehension
- | {[the given terms cannot themselves be a set]
- "{" (tset ("," tset)*)? "}" };
+ | [ { "{" tset "|" binders";" constraints "}" } ] ; set comprehension
+ | { "{" (term ("," term)*)? "}" } ; explicit set
| term ; implicit singleton
\
pred ::= { "\subset" "(" tset "," tset ")" } ; set inclusion
| { term "\in" tset } ; set membership
+ \
+ { constraints } ::= { guards ("&&" pred)? }
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/logic.tex b/src/plugins/e-acsl/doc/refman/logic.tex
index 53b4a3aacc2270e356c6c57ebba15f2d170c648b..80d0dd8aab3e3c0fe26164f2efaa000a18981d14 100644
--- a/src/plugins/e-acsl/doc/refman/logic.tex
+++ b/src/plugins/e-acsl/doc/refman/logic.tex
@@ -1,19 +1,43 @@
\begin{syntax}
- C-global-decl ::= "/*@" logic-def+ "*/"
+ C-external-declaration ::= "/*@" logic-def+ "*/"
\
logic-def ::= { logic-const-def } ;
| logic-function-def ;
| logic-predicate-def ;
+ | { lemma-def } ;
+ | { data-inv-def } ;
\
- type-expr ::= id;
+ { type-var } ::= { id } ;
\
- { logic-const-def } ::= { "logic" type-expr id "=" term ";" }
+ type-expr ::= { type-var } ; type variable
+ | id ;
+ { "<" type-expr } ;
+ { (, type-expr)* ">" } ; polymorphic type
\
- logic-function-def ::= "logic" type-expr id parameters "=" term ";"
+ { type-var-binders } ::= { "<" type-var };
+ { (, type-var)* ">" }
\
- logic-predicate-def ::= "predicate" id parameters? "=" pred ";"
+ poly-id ::= id { type-var-binders } ; polymorphic object identifier
\
- parameters ::= "(" parameter (, parameter)* ")"
+ { logic-const-def } ::= { "logic" } ;
+ { type-expr poly-id } ;
+ { "=" term ";" }
+ \
+ logic-function-def ::= "logic" ;
+ type-expr ;
+ poly-id parameters ;
+ "=" term ";"
+ \
+ logic-predicate-def ::= "predicate" ;
+ poly-id parameters? ;
+ "=" pred ";"
+ \
+ parameters ::= "(" parameter ;
+ (, parameter)* ")"
\
parameter ::= type-expr id
+ \
+ { lemma-def } ::= { clause-kind? } ;
+ { "lemma" poly-id ":" };
+ { pred ";" }
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/logicdecl.tex b/src/plugins/e-acsl/doc/refman/logicdecl.tex
new file mode 100644
index 0000000000000000000000000000000000000000..a04b81846e2e67da90e108f5ed3510afc51286d8
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/logicdecl.tex
@@ -0,0 +1,29 @@
+\begin{syntax}
+ logic-def ::= { axiomatic-decl }
+ \
+ { axiomatic-decl } ::= { "axiomatic" id "{" logic-decl* "}" }
+ \
+ { logic-decl } ::= { logic-def } ;
+ | { logic-type-decl } ;
+ | { logic-const-decl } ;
+ | { logic-predicate-decl } ;
+ | { logic-function-decl } ;
+ | { axiom-def }
+ \
+ { logic-type-decl } ::= { "type" logic-type ";" } ;
+ \
+ { logic-type } ::= { id } ;
+ | { id type-var-binders } ; polymorphic type
+ \
+ { logic-const-decl } ::= { "logic" type-expr poly-id ";" }
+ \
+ { logic-function-decl } ::=
+ { "logic" type-expr } ;
+ { poly-id parameters ";" }
+ \
+ { logic-predicate-decl } ::=
+ { "predicate" } ;
+ { poly-id parameters? ";" }
+ \
+ { axiom-def } ::= { "axiom" poly-id ":" pred ";" }
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/logicreads.tex b/src/plugins/e-acsl/doc/refman/logicreads.tex
new file mode 100644
index 0000000000000000000000000000000000000000..93e67eddb41b6f550d148e880d2f76e232d3f820
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/logicreads.tex
@@ -0,0 +1,15 @@
+\begin{syntax}
+ { logic-function-decl } ::= { "logic" type-expr poly-id };
+ { parameters reads-clause ";" }
+ \
+ { logic-predicate-decl } ::= { "predicate" poly-id };
+ { parameters? reads-clause ";" }
+ \
+ { reads-clause } ::= { "reads" locations }
+ \
+ logic-function-def ::= "logic" type-expr poly-id;
+ parameters { reads-clause } "=" term ";"
+ \
+ logic-predicate-def ::= "predicate" poly-id ;
+ parameters? { reads-clause } "=" pred ";"
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/logictypedecl.tex b/src/plugins/e-acsl/doc/refman/logictypedecl.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5a563e3242ceebb1d3436f413e8f942a5b3f1855
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/logictypedecl.tex
@@ -0,0 +1,49 @@
+\begin{syntax}
+ { logic-def } ::= { "type" logic-type = } ;
+ { logic-type-def ";" }
+ \
+ { logic-type-def } ::= { record-type } ;
+ | { sum-type } ;
+ | { product-type } ;
+ | { function-type } ;
+ | { type-expr } ; type abbreviation
+ \
+ { record-type } ::= { "{" type-expr id } ;
+ {( ";" type-expr id)* ";"? "}"}
+ \
+ { function-type } ::= { "("( type-expr };
+ { ("," type-expr )*)?")" } ;
+ { "->" type-expr }
+ \
+ { sum-type } ::= { "|"? constructor };
+ { ( "|" constructor)* }
+ \
+ { constructor } ::= { id } ; constant constructor
+ | { id } ;
+ { "(" type-expr };
+ { ("," type-expr)* ")" }; non-constant constructor
+ \
+ { product-type } ::= {"(" type-expr};
+ {("," type-expr)+ ")"} ; product type
+ \
+ term ::= {term "." id} ; record field access
+ | {"\match" term};
+ {"{" match-cases "}" } ; pattern-matching
+ | {"(" term ("," term)+ ")"} ; tuples
+ | {"{" ("." id "=" term ";")+ "}"} ; records
+ | {"\let" "(" id (, id)+ ")" "="};
+ {term ";" term}
+ \
+ { match-cases } ::= { match-case+ }
+ \
+ { match-case } ::= {"case" pat ":" term}
+ \
+ { pat } ::= { id } ; constant constructor
+ | { id "(" pat ( "," pat)* ")" } ; non-constant constructor
+ | { pat "|" pat } ; or pattern
+ | { "_" } ; any pattern
+ | { literal }
+ | { "{" ("."id "=" pat)* "}" } ; record pattern
+ | { "(" pat ( "," pat )* ")" } ; tuple pattern
+ | { pat "as" id } ; pattern binding
+\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index f9e3599b0b739122e5c63a997eaf979734a34b0f..52305b0b1612624749934aa56630790024c3e06f 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -1,28 +1,20 @@
\begin{syntax}
statement ::= "/*@" loop-annot "*/" ;
- "while" "(" C-expression ")" C-statement ;
- | "/*@" loop-annot "*/" ;
- "for";
- "(" C-expression ";" C-expression ";" C-expression ")";
- statement ;
- | "/*@" loop-annot "*/" ;
- "do" C-statement ;
- "while" "(" C-expression ")" ";"
+ C-iteration-statement ;
\
- loop-annot ::= loop-clause* ;
- { loop-behavior* } ;
- loop-variant?
+ loop-annot ::= loop-clause* { loop-behavior* } ;
+ loop-variant?
\
- loop-clause ::= loop-invariant ;
- | { loop-assigns }
+ loop-clause ::= loop-invariant | { loop-assigns } ;
+ | { loop-allocation } ;
\
- [ loop-invariant ] ::= { clause-kind? } [ "loop" "invariant" pred ";" ] ;
+ [ loop-invariant ] ::= { clause-kind? } ;
+ [ "loop" "invariant" pred ";" ] ;
\
{ loop-assigns } ::= { "loop" "assigns" locations ";" } ;
\
- { loop-behavior } ::= { "for" id ("," id)* ":" } ;
- { loop-clause* } ; \hspace{-35mm} annotation for behavior $id$
+ { loop-behavior } ::= { "for" id ("," id)* ":" loop-clause* } ; annotation for behavior $id$
\
loop-variant ::= "loop" "variant" term ";" ;
- | "loop" "variant" term "for" id ";" ; \hspace{-35mm} variant for relation $id$
+ | "loop" "variant" term "for" id ";" ; variant for relation $id$
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/macros_modern.tex b/src/plugins/e-acsl/doc/refman/macros_modern.tex
index 0034ff0ed628dbc05d558731db395e23dc9d32cd..d81957a20813ddbd451d2cc6565dc278073336b5 100644
--- a/src/plugins/e-acsl/doc/refman/macros_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/macros_modern.tex
@@ -9,6 +9,8 @@
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
\newcommand{\C}{\textsc{C}\xspace}
\newcommand{\jml}{\textsc{JML}\xspace}
+\newcommand{\Eva}{\textsc{Eva}\xspace}
+\newcommand{\Wp}{\textsc{Wp}\xspace}
\newcommand{\nodiff}{\emph{No difference with \acsl.}}
\newcommand{\except}[1]{\emph{No difference with \acsl, but #1.}}
@@ -19,17 +21,17 @@
still experimental in \acsl.}}
\newcommand{\absentexcept}[1]{\emph{No such feature in \eacsl, but #1.}}
\newcommand{\difficultwhy}[2]{\emph{#1 is usually difficult to implement, since
- it requires #2. Thus you would not wonder if most tools do not support it
- (or support it partially).}}
+ it requires #2. Thus, most tools may not support it (or may support it
+ partially).}}
\newcommand{\difficultswhy}[2]{\emph{#1 are usually difficult to implement,
- since they require #2. Thus you would not wonder if most tools do not
- support them (or support them partially).}}
-\newcommand{\difficult}[1]{\emph{#1 is usually difficult to implement. Thus
- you would not wonder if most tools do not support it (or support
- it partially).}}
-\newcommand{\difficults}[1]{\emph{#1 are usually difficult to implement. Thus
- you would not wonder if most tools do not support them (or support
+ since they require #2. Thus, most tools may not support them (or may support
them partially).}}
+\newcommand{\difficult}[1]{\emph{#1 is usually difficult to implement. Thus,
+ most tools may not support it (or may support it partially).}}
+\newcommand{\difficults}[1]{\emph{#1 are usually difficult to implement. Thus,
+ most tools may not support them (or may support them partially).}}
+\newcommand{\unefficient}[1]{\emph{#1 are unlikely evaluated efficiently at
+ runtime.}}
\newcommand{\mywarning}[1]{\paragraph{Warning:} #1}
@@ -120,16 +122,15 @@
}%
{#2}}
-\newenvironment{notimplementedenv}[1][]{%
\ifthenelse{\boolean{PrintImplementationRq}}{%
+\newenvironment{notimplementedenv}[1][]{%
\begin{changebar}%
\highlightnotimplemented%
\ifthenelse{\equal{#1}{}}{}{\def\myrq{#1}}%
- \bgroup
-}{}}%
-{\ifthenelse{\boolean{PrintImplementationRq}}{%
- \egroup%
- \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}{}}
+ \bgroup}%
+{\egroup%
+ \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}}
+{\excludecomment{notimplementedenv}}
%%% Environnements et commandes non conditionnelles
\newcommand{\experimental}{\textsc{Experimental}}
@@ -207,6 +208,7 @@
\newcommand{\blocklength}{\keywordbs{block\_length}}
\newcommand{\baseaddr}{\keywordbs{base\_addr}}
\newcommand{\comparable}{\keywordbs{comparable}}
+\newcommand{\Length}{\keywordbs{length}}
\newcommand{\N}{\ensuremath{\mathbb{N}}}
\newcommand{\ra}{\ensuremath{\rightarrow}}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 6991b746d9895195da18ac1abcf598439bea00f0..0368564d4f38b9610bbe1cd9d0b3590b1f066595 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -1,6 +1,6 @@
%; whizzy section -pdf -initex "pdflatex -ini"
\documentclass[web]{frama-c-book}
-\usepackage{hevea}
+%\usepackage{hevea}
\usepackage{ifthen}
\input{./macros_modern}
@@ -25,7 +25,7 @@
\usepackage{alltt}
\makeindex
-\newcommand{\eacsllangversion}{1.16\xspace}
+\newcommand{\eacsllangversion}{1.17\xspace}
\newcommand{\version}{\eacsllangversion\xspace}
\renewcommand{\textfraction}{0.01}
@@ -56,7 +56,7 @@
\fcaffiliationen
\vfill
\begin{flushleft}
- \textcopyright 2011-2018 CEA LIST
+ \textcopyright 2011-2021 CEA LIST
This work has been initially supported by the `Hi-Lite' FUI project (FUI AAP
9).
@@ -74,17 +74,21 @@
This document describes version \version of the \eacsl specification
language. It is based on the \acsl specification language~\cite{acsl}. Features
of both languages may still evolve in the future, even if we do our best to
-preserve backward compatibility.
+preserve backward compatibility. In particular, some features are considered
+\emph{experimental}, meaning that their syntax and semantics is not yet fixed.
+These features are marked with \experimental.
\section*{Acknowledgements}
We gratefully thank all the people who contributed to this document:
Patrick Baudin,
Bernard Botella,
+Thibaut Benjamin,
Lo\"ic Correnson,
Pascal Cuoq,
Basile Desloges,
Johannes Kanig,
+Andr\'e Maroneze,
Fonenantsoa Maurica,
David Mentr\'e,
Benjamin Monate,
diff --git a/src/plugins/e-acsl/doc/refman/memory.tex b/src/plugins/e-acsl/doc/refman/memory.tex
index c12a065c89a9bfb264616dd2ec81a83c1de2b4d8..29175c955963e3e967b0ae83301c304693916a0d 100644
--- a/src/plugins/e-acsl/doc/refman/memory.tex
+++ b/src/plugins/e-acsl/doc/refman/memory.tex
@@ -8,17 +8,13 @@
pred ::= { "\allocable" one-label? "(" term ")" };
| "\freeable" { one-label? } "(" term ")" ;
| { "\fresh" two-labels? "(" term, term ")" };
- | "\valid" { one-label? } "(" location-address ")" ;
- | "\valid_read" { one-label? } "(" location-address ")";
- | "\separated" "(" location-address "," location-addresses ")";
+ | "\valid" { one-label? } "(" locations-list ")" ;
+ | "\valid_read" { one-label? } "(" locations-list ")";
+ | "\separated" "(" location "," locations-list ")";
\
- { one-label } ::= { "{" id "}" } ;
+ { one-label } ::= { "{" label-id "}" } ;
\
- { two-labels } ::= { "{" id, id "}" } ;
- \
- location-addresses ::= location-address ("," location-address)*
- \
- location-address ::= tset
+ { two-labels } ::= { "{" label-id, label-id "}" } ;
\end{syntax}
%%% Local Variables:
diff --git a/src/plugins/e-acsl/doc/refman/model.tex b/src/plugins/e-acsl/doc/refman/model.tex
index a67cba5ae23386f275662305d800dfcd96216b0c..5cf254f45b81ce8e9733c3e8cf117ddf627e6e22 100644
--- a/src/plugins/e-acsl/doc/refman/model.tex
+++ b/src/plugins/e-acsl/doc/refman/model.tex
@@ -1,5 +1,5 @@
\begin{syntax}
- declaration ::= C-declaration ;
- | {"/*@" "model" parameter ";" "*/"} ; \hspace{-7mm} model variable
- | { "/*@" "model" C-type-name "{" parameter ";"? "}" ";" "*/" } ; model field
+ logic-def ::=
+ { "model" parameter ";" } ; model variable
+ | { "model" C-type-name "{" parameter ";"? "}" ";" } ; model field
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/predicate.tex b/src/plugins/e-acsl/doc/refman/predicate.tex
index 40c77c4af6c330c867beb51b9facb067688bbb9d..5e8bd46eb4cd266954959359a60b21c74912ede6 100644
--- a/src/plugins/e-acsl/doc/refman/predicate.tex
+++ b/src/plugins/e-acsl/doc/refman/predicate.tex
@@ -10,7 +10,7 @@
| [ pred "==>" pred ] ; \hspace{-10mm} implication
| pred "<==>" pred ; \hspace{-10mm} equivalence
| "!" pred ; \hspace{-10mm} negation
- | [ { pred "^^" pred } ] ; \hspace{-10mm} exclusive or
+ | pred "^^" pred ; \hspace{-10mm} exclusive or
| [ term "?" pred ":" pred ] ; \hspace{-10mm} ternary condition
| [ pred "?" pred ":" pred ];
| "\let" id "=" term ";" pred ; \hspace{-10mm} local binding
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index a15c8384b4a34fee6955f3a6b4bbfe4bcba1a38a..95b64e165d07ba766576e39831fadf8695fb22a6 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -17,18 +17,21 @@
\section{Logic expressions}
\label{sec:expressions}
-\except{guarded quantificatication}.
+\except{the quantifications must be guarded}
-More precisely, grammars of terms and binders presented respectively
-Figures~\ref{fig:gram:term} and~\ref{fig:gram:binders} are the same than the one
-of \acsl, while Figure~\ref{fig:gram:pred} presents grammar of predicates. The
-only difference between \eacsl and \acsl predicates are quantifications.
+More precisely, the grammars of terms and binders presented respectively
+Figures~\ref{fig:gram:term} and~\ref{fig:gram:binders} are the same than the ones
+of \acsl, while Figure~\ref{fig:gram:pred} presents the grammar of
+predicates. The only differences introduced by \eacsl with respect to \acsl are
+the fact that the quantifications that must be guarded and the introduction of
+iterators.
\begin{figure}[htbp]
\begin{cadre}
\input{term_modern.bnf}
\end{cadre}
- \caption{Grammar of terms}
+ \caption{Grammar of terms. The terminals \emph{id}, \emph{C-type-name}, and
+ various literals are the same as the corresponding \C lexical tokens.}
\label{fig:gram:term}
\end{figure}
\begin{figure}[htbp]
@@ -46,40 +49,55 @@ only difference between \eacsl and \acsl predicates are quantifications.
\end{figure}
\subsection*{Quantification}
-\eacsl quantification must be computable. They are limited to two limited forms.
-
-\begin{description}
-\item[Guarded integer quantification] Guarded universal quantification is
- denoted by
-\begin{lstlisting}
-\forall $\tau$ $x_1$,$\ldots$,$x_n$;
- $a_1$ <= $x_1$ <= $b_1$ $\ldots$ && $a_n$ <= $x_n$ <= $b_n$
- ==> p
-\end{lstlisting} and guarded existential quantification by
-\begin{lstlisting}
-\exists $\tau$ $x_1$,$\ldots$,$x_n$;
- $a_1$ <= $x_1$ <= $b_1$ $\ldots$ && $a_n$ <= $x_n$ <= $b_n$
- && p
-\end{lstlisting}
-Each variable must be guarded exactly once and the guard of $x_i$ must appear
-before the guard of $x_j$ if $i < j$ (\emph{i.e.} order of guards must follow
-order of binders).
-
-Following the definition, each quantified variable belongs to a finite
-interval. Since finite interval is only computable in practice for integers,
-this form of quantifier is limited to \texttt{integer} and its subtype. Thus
-there is no guarded quantification over \texttt{float}, \texttt{real}, \C
-pointers or logic types.
-
-\item[{\highlightnotimplemented{Iterator quantification}}] In order to iterate
- over non-integer types, \eacsl introduces a notion of $iterators$ over types:
- standard \acsl unguarded quantifications are only allowed over a type which an
- iterator is attached to.
-
- Iterators are introduced by a specific construct which attachs two sets ---
- namely \texttt{nexts} and the \texttt{guards} --- to a binary predicate over a
- type $\tau$. Both sets must have the same cardinal. This construct is
- described by the grammar of Figure~\ref{fig:gram:iterator}.
+
+{\highlightnotimplemented The general form of quantifications (called
+ generalized quantifications below), as described in
+ Fig.~\ref{fig:gram:pred},
+ is restricted to a few \emph{finite enumerable types}: the types of bound
+ variables must be \C integer types, enum types, pointer types, or their
+ aliases.
+
+\unefficient{Generalized quantification over large types (for instance, types
+ containing $2^{32}$ elements).}}
+
+In addition to generalized quantifications, a restricted form of guarded
+quantifications described in Fig.~\ref{fig:gram:guarded} is also recognized
+\emph{for (possibly infinite) enumerable types} (typically,
+\lstinline|integer|). In guarded quantifications, each bound variable must be
+guarded exactly once and, if its bounds depend on other bound variables, these
+variables must be guarded earlier or guarded by the same guard. Additionnally,
+guards are limited to bound variables, meaning that the only allowed
+identifiers $id$ are variable identifiers enclosed in the binder list.
+
+\begin{figure}[htbp]
+ \begin{cadre}
+ \input{guarded_quantif_modern.bnf}
+ \end{cadre}
+ \caption{Grammar of guarded quantifications.}
+ \label{fig:gram:guarded}
+\end{figure}
+
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{notimplementedenv}
+ Guarded quantifications over pointer types and enum types are not yet
+ implemented.
+ \end{notimplementedenv}
+}
+
+\begin{example}
+ The following predicates are (labeled) guarded quantifications:
+ \begin{itemize}
+ \item \lstinline|sorted:| \Forall{} \lstinline|integer i, j; 0 <= i <= j < len ==> a[i] <= a[j]|
+ \item {\highlightnotimplemented \lstinline|is_c:| \Exists{} \lstinline|u8 *q; p <= q < p + len && *q == (u8)c|}
+ \end{itemize}
+\end{example}
+
+\subsection*{{\highlightnotimplemented{Iterator quantification}}} For
+iterating over other data structures, \eacsl introduces a notion of $iterators$
+over types that are introduced by a specific construct which attaches two sets
+--- namely \texttt{nexts} and \texttt{guards} --- to a binary predicate over
+a type $\tau$. This construct is
+described by the grammar of Figure~\ref{fig:gram:iterator}.
\begin{figure}[htbp]
\begin{cadre}
\input{iterator_modern.bnf}
@@ -87,17 +105,20 @@ pointers or logic types.
\caption{Grammar of iterator declarations}
\label{fig:gram:iterator}
\end{figure}
- For a type $\tau$, \texttt{nexts} is a set of terms which take an argument of
- type $\tau$ and return a value of type $\tau$ which computes the next element
- in this type, while \texttt{guards} is a set of predicates which take an
- argument of type $\tau$ and are valid (resp. invalid) to continue (resp. stop)
- the iteration.
+ For a type $\tau$, \texttt{nexts} is a set of terms, and \texttt{guards} a set
+ of predicates of the same cardinal. Each term in \texttt{nexts} is a function
+ taking an argument of type $\tau$ and returning a value of type $\tau$ which
+ is a successor of its argument. Each predicate in the set \texttt{guards}
+ takes an
+ element of type $\tau$, and is valid (resp. invalid) to indicate that the
+ iteration should continue on the corresponding successor (resp. stop at the
+ given argument).
Furthermore, the guard of a quantification using an iterator must be the
predicate given in the definition of the iterator. This abstract binary
predicate takes two arguments of the same type. One of them must be unnamed by
using a wildcard (character underscore \texttt{'\_'}). The unnamed argument
- must be binded to the guantifier, while the other corresponds to the term from
+ must be bound to the quantifier, while the other corresponds to the term from
which the iteration begins.
\begin{example}
The following example introduces binary trees and a predicate which is valid
@@ -105,10 +126,6 @@ pointers or logic types.
\cinput{link.c}
\end{example}
-\item[{\highlightnotimplemented{Unguarded quantification}}] They are only
- allowed over boolean and char.
-\end{description}
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Operators precedence}
@@ -178,8 +195,8 @@ The semantics of all the below predicates are undefined:
\end{itemize}
\end{example}
-Furthermore, \C-like operators \lstinline|&&|, \lstinline+||+, \lstinline|^^|
-and \lstinline|_ ? _ : _| are lazy like in \C: their right members are evaluated
+Furthermore, \C-like operators \lstinline|&&|, \lstinline+||+, and
+\lstinline|_ ? _ : _| are lazy like in \C: their right members are evaluated
only if required. Thus the amount of undefinedness is limited. Consequently,
predicate \lstinline|p ==> q| is also lazy since it is equivalent
to \lstinline+!p || q+. It is also the case for guarded quantifications since
@@ -187,13 +204,13 @@ guards are conjunctions and for ternary condition since it is equivalent to a
disjunction of implications.
\begin{example}\label{ex:semantics}
-Below, the first, second and fourth predicates are invalid while the third
-one is valid:
+ All the predicates below are well defined. The first, second and fourth
+ predicates are invalid, whereas the third one is valid:
\begin{itemize}
\item \lstinline|\false && 1/0 == 1/0|
\item \lstinline|\forall integer x, -1 <= x <= 1 ==> 1/x > 0|
\item \lstinline|\forall integer x, 0 <= x <= 0 ==> \false ==> -1 <= 1/x <= 1|
-\item \lstinline|\exists integer x, 1 <= x <= 0 && -1 <= 1/x <= 1|
+\item \lstinline|\exists integer x, 1 <= x <= 0 && -1 <= 1/0 <= 1|
\end{itemize}
In particular, the second one is invalid since the quantification is in fact an
enumeration over a finite number of elements, it amounts to
@@ -202,7 +219,7 @@ invalid, so the rest of the conjunction (and in particular 1/0) is not
evaluated. The fourth one is invalid since it is an existential quantification
over an empty range.
-\emph{A contrario} the semantics of predicates below is undefined:
+\emph{A contrario} the semantics of the predicates below is undefined:
\begin{itemize}
\item \lstinline|1/0 == 1/0 && \false|
\item \lstinline|-1 <= 1/0 <= 1 ==> \true|
@@ -224,28 +241,31 @@ Below, the first term is well-defined, while the second one is undefined.
\paragraph{Handling undefinedness in tools}
It is the responsibility of each tool which interprets \eacsl to ensure that an
-undefined term is never evaluated. For instance, they may exit with a proper
-error message or, if they generate \C code, they may guard each generated
+undefined term is never evaluated. For instance, it may exit with a proper
+error message or, if it generates \C code, it may guard each generated
undefined \C expression in order to be sure that they are always safely used.
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ The \eacsl plug-in of \framac generates such guards. \notimplemented{Yet,
+ a few guards are still missing.}
+
+}
+
This behavior is consistent with both \acsl~\cite{acsl} and mainstream
specification languages for runtime assertion checking like
\jml~\cite{jml}. Consistency means that, if it exists and is defined, the \eacsl
predicate corresponding to a valid (resp. invalid) \acsl predicate is valid
-(resp. invalid). Thus it is possible to reuse tools interpreting \acsl like the
-\framac's value analysis plug-in~\cite{value} in order to interpret \eacsl, and
+(resp. invalid). Thus it is possible to reuse tools interpreting \acsl (e.g.,
+\framac's \Eva~\cite{eva} or \Wp~\cite{wp} in order to interpret \eacsl, and
it is also possible to perform runtime assertion checking of \eacsl predicates
in the same way than \jml predicates. Reader interested by the implications
-(especially issues) of such a choice may read articles of Patrice
-Chalin~\cite{chalin05,chalin07}.
+(especially issues) of such a choice may read the articles of Patrice
+Chalin on that topic~\cite{chalin05,chalin07}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Typing}\label{sec:typing}
-\except{no user-defined types}
-
-It is not possible to define logic types introduced by the specification writer
-(see Section~\ref{sec:logicspec}).
+\nodiff
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -256,15 +276,24 @@ It is not possible to define logic types introduced by the specification writer
\subsection{Real numbers and floating point numbers}
\label{sec:reals}
-\nodiff
+\except{no quantification over real numbers and floating point numbers}
-\difficults{Exact real numbers and even floating point numbers}
+\difficults{Exact real numbers and even operations over floating point numbers}
-\begin{notimplementedenv}
- Real numbers beyond rationals are currently not supported by the \eacsl
- plug-in. Only rationals (in $\mathbb{Q}$) and floating point numbers are
- supported.
-\end{notimplementedenv}
+More precisely, most real numbers are not representable at runtime with an
+infinite precisions. Consequently, most operations over them (e.g., equality)
+cannot be computed at runtime with an arbitrary precision. In such cases, it is
+the responsibility of each tool which interprets \eacsl to specify the
+level of precision (e.g., $1e^{-6}$) up to which it is sound, and/or to emit
+undefinitive verdicts (e.g., ``unknown'').
+
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{notimplementedenv}
+ Only floating point numbers (e.g., \texttt{0.1f}), rationals numbers (in
+ $\mathbb{Q}$) and operations over them are supported by the \eacsl
+ plug-in. Real numbers that are irrational numbers are not supported.
+ \end{notimplementedenv}
+}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -282,13 +311,17 @@ It is not possible to define logic types introduced by the specification writer
\difficults{Logic arrays without an explicit length}
-\begin{notimplementedenv}
- The \lstinline|\length| function is currently not supported by the \eacsl
- plug-in.
-
- The comparison of unions and structures is currently not supported by the
- \eacsl plug-in.
-\end{notimplementedenv}
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{notimplementedenv}
+ The following constructs are currently not supported by the \eacsl plug-in:
+ \begin{itemize}
+ \item built-in function \Length;
+ \item comparisons of unions and structures;
+ \item functional updates;
+ \item conversions of structure to structure.
+ \end{itemize}
+ \end{notimplementedenv}
+}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -298,12 +331,12 @@ It is not possible to define logic types introduced by the specification writer
\label{sec:fn-behavior}
\index{function contract}\index{contract}
-\except{no \lstinline|terminates|}
+\except{no clause \lstinline|terminates|}
-Figure~\ref{fig:gram:contracts} shows grammar of function
-contracts. This is a simplified version of \acsl one without
-\lstinline|terminates| clauses. Section~\ref{sec:termination} explains why
-\eacsl has no \lstinline|terminates| clause.
+Figure~\ref{fig:gram:contracts} shows the grammar of function contracts. This is
+a simplified version of \acsl one without \lstinline|terminates|
+clauses. Section~\ref{sec:termination} explains why \eacsl has no
+\lstinline|terminates| clause.
\begin{figure}[htbp]
\begin{cadre}
@@ -322,8 +355,8 @@ contracts. This is a simplified version of \acsl one without
\nodiff
-Figure~\ref{fig:gram:oldandresult} summarizes grammar extension of terms with
-\lstinline|\old| and \lstinline|\result|.
+Figure~\ref{fig:gram:oldandresult} summarizes the grammar extension of terms
+with \lstinline|\old| and \lstinline|\result|.
\begin{figure}[htbp]
\begin{cadre}
\input{oldandresult_modern.bnf}
@@ -339,7 +372,7 @@ Figure~\ref{fig:gram:oldandresult} summarizes grammar extension of terms with
\nodiff
-\difficultwhy{\notimplemented{\lstinline|\\assigns|}}{the implementation of a
+\difficultwhy{\notimplemented{\lstinline|assigns|}}{the implementation of a
memory model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -358,11 +391,15 @@ Figure~\ref{fig:gram:oldandresult} summarizes grammar extension of terms with
\except{ranges and \notimplemented{set comprehensions} are limited in order to
be finite}
-Figure~\ref{fig:gram:locations} describes grammar of sets of terms. The only
-differences with \acsl are that both lower and upper bounds of ranges are
-mandatory and that the predicate inside set comprehension must be guarded and
-bind only one variable. In that way, each set of terms is finite and their
-members easily identifiable.
+Figure~\ref{fig:gram:locations} describes the grammar of sets of terms. There
+are two differences with \acsl:
+\begin{itemize}
+\item ranges necessarily have lower and upper bounds;
+\item a guard for each binder is required when defining set comprehension. The
+ requested constraints for guards are the very same than the ones for
+ quantifications.
+\end{itemize}
+
\begin{figure}[htbp]
\fbox{\begin{minipage}{0.97\textwidth}
\input{loc_modern.bnf}
@@ -373,21 +410,24 @@ members easily identifiable.
\begin{notimplementedenv}
\begin{example}\label{ex:tset}
-The set \lstinline*{ x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }* denotes the
-set of all integers between 0 and 9 and between 20 and 29.
+The set \lstinline*{ x | integer x; 0 <= x <= 10 && x % 2 == 0}* denotes the
+set of even integers between 0 and 10.
\end{example}
\end{notimplementedenv}
-\begin{notimplementedenv}
- Ranges are currently only supported in memory built-ins described in
- Section~\ref{subsec:memory},~\ref{sec:initialized} and~\ref{sec:dangling}.
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{notimplementedenv}
+ Ranges are currently only supported in memory built-ins described in
+ Section~\ref{subsec:memory},~\ref{sec:initialized} and~\ref{sec:dangling}.
+ \end{notimplementedenv}
-\begin{example}
-The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that
-the ten first cells of the array \lstinline|t| are valid. Writing the term
-\lstinline|&t[0 .. 9]| alone, outside any memory built-in, is not yet supported.
-\end{example}
-\end{notimplementedenv}
+ \begin{example}
+ The predicate \lstinline|\\valid(&t[0 .. 9])| is supported and denotes
+ that the ten first cells of the array \lstinline|t| are valid. Writing the
+ term \lstinline|&t[0 .. 9]| alone, outside any memory built-in, is not yet
+ supported.
+ \end{example}
+}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -408,7 +448,7 @@ the ten first cells of the array \lstinline|t| are valid. Writing the term
\indextt{assert}
\nodiff
-Figure~\ref{fig:gram:assertions} summarizes grammar for assertions.
+Figure~\ref{fig:gram:assertions} summarizes the grammar for assertions.
\begin{figure}[htbp]
\begin{cadre}
\input{assertions_modern.bnf}
@@ -424,7 +464,7 @@ Figure~\ref{fig:gram:assertions} summarizes grammar for assertions.
\except{loop invariants lose their inductive nature}
-Figure~\ref{fig:gram:loops} shows grammar for loop annotations. There is no
+Figure~\ref{fig:gram:loops} shows the grammar for loop annotations. There is no
syntactic difference with \acsl.
\begin{figure}[htbp]
\begin{cadre}
@@ -434,34 +474,36 @@ syntactic difference with \acsl.
\label{fig:gram:loops}
\end{figure}
-\difficultwhy{\notimplemented{\lstinline|loop assigns|}}{the implementation of a
- memory model}
+\difficultswhy{\notimplemented{\lstinline|loop allocation|} and
+ \notimplemented{\lstinline|loop assigns|}}{the implementation of a memory
+ model}
\subsubsection{Loop invariants}
\index{invariant} The semantics of loop invariants is the same than the one
defined in \acsl, except that they are not inductive. More precisely, if one
-does not take care of side effects (semantics of specifications about side
+does not take care of side effects (the semantics of specifications about side
effects in loop is the same in \eacsl than the one in \acsl), a loop invariant
$I$ is valid in \acsl if and only if:
\begin{itemize}
\item $I$ holds before entering the loop; and
\item if $I$ is assumed true in some state where the loop condition $c$ is also
- true, and if execution of the loop body in that state ends normally at the end
- of the body or with a "continue" statement, $I$ is true in the resulting
+ true, and if the execution of the loop body in that state ends normally at the
+ end of the body or with a "continue" statement, $I$ is true in the resulting
state.
\end{itemize}
In \eacsl, the same loop invariant $I$ is valid if and only if:
\begin{itemize}
\item $I$ holds before entering the loop; and
-\item if execution of the loop body in that state ends normally at the end of
- the body or with a "continue" statement, $I$ is true in the resulting state.
+\item if the execution of the loop body in that state ends normally at the end
+ of the body or with a "continue" statement, $I$ is true in the resulting
+ state.
\end{itemize}
Thus the only difference with \acsl is that \eacsl does not assume that the
invariant previously holds when one checks that it holds at the end of the loop
-body. In other words a loop invariant \lstinline|I| is equivalent to put an
+body. In other words a loop invariant \lstinline|I| is equivalent to putting an
assertion \lstinline|I| just before entering the loop and at the very end of the
loop body.
@@ -481,8 +523,10 @@ loop invariants are not inductive.
\subsubsection{General inductive invariant}
\label{sec:generalized-invariants}
-Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
-\begin{figure}[t]
+The syntax of this kind of invariant is shown
+Figure~\ref{fig:advancedinvariants}.
+
+\begin{figure}[htbp]
\begin{cadre}
\input{generalinvariants_modern.bnf}
\end{cadre}
@@ -490,8 +534,8 @@ Syntax of these kinds of invariant is shown Figure~\ref{fig:advancedinvariants}
\label{fig:advancedinvariants}
\end{figure}
-In \eacsl, these kinds of invariants put everywhere in a loop body is exactly
-equivalent to an assertion.
+In \eacsl, a general inductive invariant may be written everywhere in a loop
+body, and is exactly equivalent to writing an assertion.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -500,46 +544,53 @@ equivalent to an assertion.
\except{no forward references}
-The construct \verb|\at(t,id)| (where \verb|id| is a regular C label, a label
+The construct \verb|\at(t,id)| (where \verb|id| is a regular \C label, a label
added within a ghost statement or a default logic label)
follows the same rule than its \acsl counterpart, except that a more restrictive
scoping rule must be respected in addition to the standard \acsl scoping rule:
-when evaluating \verb|\at(t,id)| at a propram point $p$, the program point $p'$
-denoted by \verb|id| must be executed after $p$ the program execution flow.
+\begin{itemize}
+\item when evaluating \verb|\at(t,id)| at a propram point $p$, the program point
+ $p'$ denoted by \verb|id| must be reached before $p$ in the program execution
+ flow; and
+\item when evaluating \verb|\at(t,id)|, for each \C left-value $x$ that
+ contributes to the definition of a (non-ghost) logic variable involved in $t$,
+ the equality \verb|\at(x,id) == \at(x,Here)| must hold, i.e. the value of $x$
+ must not be modified between the program points \verb|id| and \verb|Here|.
+\end{itemize}
-\begin{example}
-In the following example, both assertions are accepted and valid in \acsl, but
-only the first one is accepted and valid in \eacsl since evaluating the term
-\verb|\at(*(p+\at(*q,Here)),L1)| at \verb|L2| requires to evaluate the term
- \verb|\at(*q,Here)| at \verb|L1|: that is forbidden since \verb|L1| is executed
- before \verb|L2|.
-\cinput{at.c}
+Below, the first example illustrates the first constraint, whereas the second
+example illustrates the second constraint.
+\begin{example}
+ In the following example, both assertions are accepted and valid in \acsl, but
+ only the first one is accepted and valid in \eacsl since evaluating the term
+ \verb|\at(*(p+\at(*q,Here)),L1)| at \verb|L2| requires to evaluate the term
+ \verb|\at(*q,Here)| at \verb|L1|: that is forbidden since \verb|L1| is
+ executed before \verb|L2|. \cinput{at.c}
\end{example}
-For the time being, \verb|\at| can be applied to any term or predicate that uses
-quantified variables, let-binded variables and C variables.
-
\begin{example}
-The \verb|\at| construct of the following example is supported.
-\cinput{at_on-purely-logic-variables.c}
-
+ In the following example, the first assertion is supported, while the second
+ one is not supported. Indeed, in the second assertion, the guard defining the
+ logic variable \verb|u| depends on \verb|n| whose value is modified between
+ \verb|L1| and \verb|L2|.
+ \cinput{at_on-purely-logic-variables.c}
\end{example}
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{notimplementedenv}
+ Any \lstinline|\\at| construct involving a logic variable whose definition
+ depends on a \C variable is currently unsupported by plug-in \eacsl.
-\begin{notimplementedenv}
-However, quantified variables that use C variables in their bounds and
-let-binded variables that use C variables in their definition
-are not yet supported.
-
-\begin{example}
-The \verb|\at| construct of the following example is \emph{not yet} supported
-since the quantified variable \verb|i| uses the C variable \verb|n| in the
-definition of its upper bound.
-\cinput{at_on-purely-logic-variables_not-yet.c}
-
-\end{example}
-\end{notimplementedenv}
+ \begin{example}
+ The \lstinline|\\old| construct (special case of \lstinline|\\at|) of the
+ following example is \emph{not yet} supported since the guard of the
+ quantified variable \lstinline|i| depends on the \C variable \lstinline|n|
+ in the definition of its upper bound.
+ \cinput{at_on-purely-logic-variables_not-yet.c}
+ \end{example}
+ \end{notimplementedenv}
+}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -549,7 +600,7 @@ definition of its upper bound.
\nodiff
-Figure~\ref{fig:gram:stcontracts} shows grammar of statement contracts.
+Figure~\ref{fig:gram:stcontracts} shows the grammar of statement contracts.
\begin{figure}[htbp]
\begin{cadre}
@@ -590,7 +641,8 @@ Figure~\ref{fig:gram:stcontracts} shows grammar of statement contracts.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Non-terminating functions}
-\absentexperimental
+\absentwhy{whether a function is guaranteed to terminate if some predicate $p$
+ holds is not a monitorable property}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -600,11 +652,9 @@ Figure~\ref{fig:gram:stcontracts} shows grammar of statement contracts.
\label{sec:logicspec}
\index{logic specification}\index{specification}
-\limited{stable and computable features}
+\nodiff
-Figure~\ref{fig:gram:logic} presents grammar of logic definitions. This is the
-same than the one of \acsl without polymorphic definitions, lemmas, nor
-axiomatics.
+Figure~\ref{fig:gram:logic} presents the grammar of logic definitions.
\begin{figure}[htbp]
\fbox{\begin{minipage}{0.97\linewidth}\vfill \input{logic_modern.bnf}
@@ -620,28 +670,63 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Lemmas}
-\absentwhy{lemmas are user-given propositions. They are written usually to help
- theorem provers to establish validity of specifications. Thus they are mostly
- useful for verification activities based on deductive methods which are out of
- the scope of \eacsl. Furthermore, they often requires human help to be proven,
- although \eacsl targets are automatic tools}
+\subsection{\notimplemented{Lemmas}}
+\nodiff
+
+Lemmas are verified before running the function \lstinline|main| but after
+initializing global variables.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Inductive predicates}\label{sec:inductive}
-\absentwhy{inductive predicates are not computable if they really use their
- inductive nature}
+\subsection{\notimplemented{Inductive predicates}}
+\label{sec:inductivepredicates}
+\index{inductive predicates}
+\experimental
+
+\nodiff
+
+Figure~\ref{fig:gram:inductive} presents the grammar of inductive predicates.
+
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\linewidth}\vfill \input{inductive_modern.bnf}
+ \vfill\end{minipage}}
+ \caption{Grammar for inductive predicates}
+\label{fig:gram:inductive}
+\end{figure}
+
+Inductive predicates in all their generality are not monitorable. Therefore,
+future versions of this document will restrict them syntactically (e.g., to
+definite Horn clauses (\url{http://en.wikipedia.org/wiki/Horn_clause}) and/or
+through semantic criteria.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Axiomatic definitions}
-\absentwhy{by nature, an axiomatic is not computable}
+\subsection{\notimplemented{Axiomatic definitions}}
+\label{sec:axiomatic}
+\experimental
+
+\nodiff
+
+Figure~\ref{fig:gram:logicdecl} presents the grammar of axiomatic definitions.
+
+\begin{figure}[htbp]
+ \fbox{\begin{minipage}{0.97\linewidth}\vfill \input{logicdecl_modern.bnf}
+ \vfill\end{minipage}}
+ \caption{Grammar for axiomatic declarations}
+\label{fig:gram:logicdecl}
+\end{figure}
+
+Axiomatic definitions in all their generality are not monitorable. Therefore,
+future versions of this document will restrict them syntactically and/or
+through semantic criteria.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Polymorphic logic types}
-\absentexperimental
+\subsection{\notimplemented{Polymorphic logic types}}
+\label{sec:polym-logic-types}
+\index{type!polymorphic}
+\index{polymorphism}
+\nodiff
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -651,13 +736,44 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Higher-order logic constructions}
-\absentexperimental
+\subsection{\notimplemented{Higher-order logic constructions}}
+\label{sec:higherorder}
+
+\experimental
+
+\nodiff
+
+Figure~\ref{fig:gram:higherorder} introduces new term constructs for
+higher-order logic.
+
+\begin{figure}[htp]
+ \begin{cadre}
+ \input{higherorder_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for higher-order constructs}
+\label{fig:gram:higherorder}
+\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Concrete logic types}\label{sec:concrete-logic-types}
-\absentexperimental
+\subsection{\notimplemented{Concrete logic types}}
+\label{sec:concrete-logic-types}
+\index{type!concrete}
+\experimental
+
+\nodiff
+
+Figure~\ref{fig:gram:logictype} introduces new constructs for defining logic
+types and the associated new terms.
+
+\begin{figure}[htp]
+ \begin{cadre}
+ \index{type!record}\index{type!sum}
+ \input{logictypedecl_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for concrete logic types and pattern-matching}
+\label{fig:gram:logictype}
+\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -672,8 +788,24 @@ axiomatics.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Memory footprint specification: \texorpdfstring{\lstinline|reads|}{reads} clause}
-\absentexperimental
+\subsection{\notimplemented{Memory footprint specification: \texorpdfstring{\lstinline|reads|}{reads} clause}}
+\label{sec:reads}
+\experimental
+
+\nodiff
+
+Figure~\ref{fig:gram:logicreads} introduces \lstinline|reads| clauses.
+
+\begin{figure}[htp]
+ \begin{cadre}
+ \input{logicreads_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for logic declarations with \lstinline|reads| clauses}
+\label{fig:gram:logicreads}
+\end{figure}
+
+\difficultswhy{\notimplemented{read clauses}}{the implementation of a memory
+ model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -688,7 +820,7 @@ axiomatics.
\section{Pointers and physical adressing}
\label{sec:pointers}
-\except{separation}
+\nodiff
Figure~\ref{fig:gram:memory} shows the additional constructs for terms and
predicates which are related to memory location.
@@ -707,10 +839,8 @@ predicates which are related to memory location.
\label{sec:memory} % for correctness of \changeinsection in Changes
\nodiff
-\difficultswhy{\lstinline|\\base\_addr|,
- \lstinline|\\block\_length|, \lstinline|\\valid|,
- \lstinline|\\valid_read| and
- \lstinline|\\offset|}{the implementation of a memory model}
+\difficultswhy{All memory-related built-in functions and predicates}{the
+ implementation of a memory model}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -721,22 +851,34 @@ predicates which are related to memory location.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Dynamic allocation and deallocation}
-\difficultswhy{All these constructs}{the implementation of a memory model}
+\subsection{\notimplemented{Dynamic allocation and deallocation}}
\label{sec:alloc-dealloc}
\nodiff
+\difficultswhy{All these constructs}{the implementation of a memory model}
+
+Figure~\ref{fig:gram:allocation} introduces grammar for dynamic allocations and
+deallocations.
+
+\begin{figure}[htp]
+ \begin{cadre}
+ \input{allocation_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for dynamic allocations and deallocations}
+\label{fig:gram:allocation}
+\end{figure}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Sets and lists}
+\section{\notimplemented{Sets and lists}}
\index{location}
-\subsection{Finite sets}
+\subsection{\notimplemented{Finite sets}}
\nodiff
-\subsection{Finite lists}
+\subsection{\notimplemented{Finite lists}}
\nodiff
Figure~\ref{fig:gram:list} shows the notations for built-in lists.
@@ -758,7 +900,7 @@ Figure~\ref{fig:gram:list} shows the notations for built-in lists.
\nodiff
-Figure~\ref{fig:gram:abrupt} shows grammar of abrupt termination.
+Figure~\ref{fig:gram:abrupt} shows the grammar of abrupt terminations.
\begin{figure}[htbp]
\begin{cadre}
@@ -772,8 +914,21 @@ Figure~\ref{fig:gram:abrupt} shows grammar of abrupt termination.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Dependencies information}
-\absentexperimental
+\section{\notimplemented{Dependencies information}}
+\label{sec:func-dep}
+\experimental
+
+\nodiff
+
+Figure~\ref{fig:gram:dep} shows the grammar for dependencies information.
+
+\begin{figure}[htp]
+ \begin{cadre}
+ \input{dependencies_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for dependencies information}
+\label{fig:gram:dep}
+\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -796,6 +951,8 @@ invariants.
\label{fig:gram:datainvariants}
\end{figure}
+\unefficient{strong invariants}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Semantics}
@@ -809,7 +966,7 @@ invariants.
\nodiff
-Figure~\ref{fig:gram:model} summarizes grammar for declarations of model
+Figure~\ref{fig:gram:model} summarizes the grammar for declarations of model
variables and fields.
\begin{figure}[htbp]
\fbox{\begin{minipage}{0.97\linewidth}
@@ -827,10 +984,10 @@ variables and fields.
\label{sec:ghost}
\index{ghost}
-\except{no specific construct for volatile variables}
+\nodiff
-Figure~\ref{fig:gram:ghost} summarizes grammar for ghost statements which is the
-same than the one of \acsl.
+Figure~\ref{fig:gram:ghost} summarizes the grammar for ghost statements which is
+the same than the one of \acsl.
\begin{figure}[htbp]
\fbox{\begin{minipage}{0.98\linewidth}
\input{ghost_modern.bnf}
@@ -841,8 +998,18 @@ same than the one of \acsl.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Volatile variables}
-\absentexperimental
+\subsection{\notimplemented{Volatile variables}}
+\label{sec:volatile-variables}
+\indextt{volatile}
+
+Figure~\ref{fig:gram:volatile} summarizes the grammar for volatile constructs.
+\begin{figure}[htp]
+ \begin{cadre}
+ \input{volatile-gram_modern.bnf}
+ \end{cadre}
+ \caption{Grammar for volatile constructs}
+\label{fig:gram:volatile}
+\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -854,7 +1021,14 @@ same than the one of \acsl.
\difficultwhy{\lstinline|\\initialized|}{the implementation of a memory model}
-\section{Dangling pointers}
+\ifthenelse{\boolean{PrintImplementationRq}}{%
+ \begin{notimplementedenv}
+ The \framac plug-in \eacsl does not support labels as arguments of
+ \lstinline|\\initialized|.
+ \end{notimplementedenv}
+}
+
+\section{\notimplemented{Dangling pointers}}
\label{sec:dangling}
\nodiff
@@ -867,14 +1041,15 @@ same than the one of \acsl.
\section{Well-typed pointers}
\label{sec:typedpointers}
-\absentexperimental
+\absentwhy{it would require the implementation of a \C type system at runtime}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Logic attribute annotations}
-\absentexperimental
+\absentwhy{logic attributes are implementation dependent; therefore their
+ meaning cannot be guessed by a general-purpose (runtime) verification tool}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/doc/refman/st_contracts.tex b/src/plugins/e-acsl/doc/refman/st_contracts.tex
index 8aefcbe9f322ac060e59ba1f56a97766fcff513f..882a6cab9d60255fcafb6119794d86bfd82c2fda 100644
--- a/src/plugins/e-acsl/doc/refman/st_contracts.tex
+++ b/src/plugins/e-acsl/doc/refman/st_contracts.tex
@@ -1,7 +1,7 @@
\begin{syntax}
statement ::= "/*@" statement-contract "*/" statement
\
- [ statement-contract ] ::= {("for" id ("," id)* ":")?} requires-clause* ;
+ statement-contract ::= {("for" id ("," id)* ":")?} requires-clause* ;
simple-clause-stmt* named-behavior-stmt* ;
completeness-clause*
\
diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex
index 67e3edea7855fd98c34194346fdc744dac7b59ab..69e73ca5054606bf29f8503c114f83940f9a8c3b 100644
--- a/src/plugins/e-acsl/doc/refman/term.tex
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -1,14 +1,16 @@
\begin{syntax}
literal ::= { "\true" } | { "\false" } ; boolean constants
- | integer ; integer constants
- | real ; real constants
- | string ; string constants
- | character ; character constants
+ | integer ; (lexical) integer constants
+ | real ; (lexical) real constants
+ | string ; (lexical) string constants
+ | character ; (lexical) character constants
\
- bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | "<<" | ">>";
+ bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] ;
| "==" | "!=" | "<=" | ">=" | ">" | "<" ;
| [ "&&" ] | [ "||" ] | [ "^^" ] ; boolean operations
- | "&" | "|" | "-->" | "<-->" | "^" ; bitwise operations
+ | "<<" | ">>" ;
+ | "&" | "|" | "-->"
+ | "<-->" | "^" ; bitwise operations
\
unary-op ::= "+" | "-" ; unary plus and minus
| "!" ; boolean negation
@@ -17,11 +19,12 @@
| "&" ; address-of operator
\
term ::= literal ; literal constants
- | id ; variables
+ | id ; variables, function names
| unary-op term ;
| term bin-op term ;
| term "[" term "]" ; array access
- | { "{" term "\with" "[" term "]" "=" term "}" } ; array functional modifier
+ | { "{" term } ;
+ { "\with" "[" term "]" "=" term "}" } ; array functional modifier
| term "." id ; structure field access
| { "{" term "\with" "."id "=" term "}" } ; field functional modifier
| term "->" id ;
@@ -31,7 +34,11 @@
| [ term "?" term ":" term ] ; ternary condition
| "\let" id "=" term ";" term ; local binding
| "sizeof" "(" term ")" ;
- | "sizeof" "(" C-type-name ")" ;
+ | "sizeof" "(" C-type-expr ")" ;
| id ":" term ; syntactic naming
| string ":" term ; syntactic naming
+ \
+ poly-id ::= id ;
+ \
+ ident ::= id ;
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/volatile-gram.tex b/src/plugins/e-acsl/doc/refman/volatile-gram.tex
new file mode 100644
index 0000000000000000000000000000000000000000..c4f9b8dc027d3b0de363394e95194a821209049a
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/volatile-gram.tex
@@ -0,0 +1,8 @@
+\begin{syntax}
+ logic-def ::= { "//@" "volatile" locations ("reads" ident)? ("writes" ident)?";" }
+\end{syntax}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End: