Merge branch 'feature/e-acsl/refman-upgrade-vanadium' into 'stable/vanadium'

Feature/e acsl/refman upgrade vanadium

See merge request frama-c/frama-c!3264

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 #

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 ";" }
     \

src/plugins/e-acsl/doc/refman/allocation.tex

+\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}

src/plugins/e-acsl/doc/refman/assertions.tex

 \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}

src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c

 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;
 }

src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c

 /*@ 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);

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.)},

src/plugins/e-acsl/doc/refman/changes_modern.tex

 \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}

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.

src/plugins/e-acsl/doc/refman/data_invariants.tex

 \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 ";" } 

src/plugins/e-acsl/doc/refman/dependencies.tex

+\begin{syntax}
+{ assigns-clause } ::= { "assigns" locations-list ("\from" locations )? ";" } ;
+                 | { "assigns" term "\from" locations "=" term ";" }
+\end{syntax}

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 }
   \

src/plugins/e-acsl/doc/refman/ghost.tex

 \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}

src/plugins/e-acsl/doc/refman/guarded_quantif.tex

+\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}

src/plugins/e-acsl/doc/refman/higherorder.tex

+\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}

src/plugins/e-acsl/doc/refman/inductive.tex

+\begin{syntax}
+  logic-def ::= { inductive-def }
+  \
+  { inductive-def } ::= { "inductive" } ;
+  { poly-id parameters? "{" indcase* "}" }
+  \
+  { indcase } ::= { "case" poly-id ":" pred ";" }
+\end{syntax}

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}

src/plugins/e-acsl/doc/refman/iterator.tex

 \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}

src/plugins/e-acsl/doc/refman/list-gram.tex

 \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}

src/plugins/e-acsl/doc/refman/loc.tex

 \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}