From 6ab782b32e644fd528c71e6b79ad9d4ca30d0a93 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 25 Mar 2021 15:41:32 +0100
Subject: [PATCH] [eacsl] Update grammars to stay in the frames
---
src/plugins/e-acsl/doc/refman/fn_behavior.tex | 10 ++---
src/plugins/e-acsl/doc/refman/model.tex | 2 +-
src/plugins/e-acsl/doc/refman/predicate.tex | 40 +++++++++----------
3 files changed, 26 insertions(+), 26 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index 8411919520d..3831ef9c22a 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -1,7 +1,7 @@
\begin{syntax}
- [ function-contract ] ::= requires-clause*
- { decreases-clause? } simple-clause*
- named-behavior* completeness-clause*
+ [ function-contract ] ::= requires-clause* ;
+ { decreases-clause? } simple-clause* ;
+ named-behavior* completeness-clause* ;
\
clause-kind ::= "check" | "admit"
\
@@ -9,7 +9,7 @@
\
{ decreases-clause } ::= { "decreases" term ("for" id)? ";" }
\
- [ simple-clause ] ::= { assigns-clause } | ensures-clause
+ [ simple-clause ] ::= { assigns-clause } | ensures-clause ;
| { allocation-clause} | { abrupt-clause }
\
{ assigns-clause } ::= { "assigns" locations ";" }
@@ -26,6 +26,6 @@
\
assumes-clause ::= "assumes" pred ";"
\
- completeness-clause ::= "complete" "behaviors" (id (","id)*)? ";"
+ completeness-clause ::= "complete" "behaviors" (id (","id)*)? ";" ;
| "disjoint" "behaviors" (id (","id)*)? ";"
\end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/model.tex b/src/plugins/e-acsl/doc/refman/model.tex
index d46d192e91e..a67cba5ae23 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 ";" "*/"} ; model variable
+ | {"/*@" "model" parameter ";" "*/"} ; \hspace{-7mm} 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 c89a1ed2979..40c77c4af6c 100644
--- a/src/plugins/e-acsl/doc/refman/predicate.tex
+++ b/src/plugins/e-acsl/doc/refman/predicate.tex
@@ -2,31 +2,31 @@
rel-op ::= "==" | "!=" | "<=" | ">=" | ">" | "<"
\
pred ::= "\true" | "\false" ;
- | term (rel-op term)+ ; comparisons
- | id "(" term ("," term)* ")" ; predicate application
- | "(" pred ")" ; parentheses
- | [ pred "&&" pred ] ; conjunction
- | [ pred "||" pred ] ; disjunction
- | [ pred "==>" pred ] ; implication
- | pred "<==>" pred ; equivalence
- | "!" pred ; negation
- | [ { pred "^^" pred } ] ; exclusive or
- | [ term "?" pred ":" pred ] ; ternary condition
+ | term (rel-op term)+ ; \hspace{-10mm} comparisons
+ | id "(" term ("," term)* ")" ; \hspace{-10mm} predicate application
+ | "(" pred ")" ; \hspace{-10mm} parentheses
+ | [ pred "&&" pred ] ; \hspace{-10mm} conjunction
+ | [ pred "||" pred ] ; \hspace{-10mm} disjunction
+ | [ pred "==>" pred ] ; \hspace{-10mm} implication
+ | pred "<==>" pred ; \hspace{-10mm} equivalence
+ | "!" pred ; \hspace{-10mm} negation
+ | [ { pred "^^" pred } ] ; \hspace{-10mm} exclusive or
+ | [ term "?" pred ":" pred ] ; \hspace{-10mm} ternary condition
| [ pred "?" pred ":" pred ];
- | "\let" id "=" term ";" pred ; local binding
+ | "\let" id "=" term ";" pred ; \hspace{-10mm} local binding
| { "\let" id "=" pred ";" pred };
- | [ "\forall" binders ";" ] ;
- [ integer-guards "==>" pred ]; univ. integer quantification
+ | [ "\forall" binders ";" ] ;
+ [ integer-guards "==>" pred ]; \hspace{-10mm} univ. integer quantification
| [ "\exists" binders ";" ];
- [ integer-guards "&&" pred ] ; exist. integer quantification
+ [ integer-guards "&&" pred ] ; \hspace{-10mm} exist. integer quantification
| [ { "\forall" binders ";" } ] ;
- [ { iterator-guard "==>" pred } ]; univ. iterator quantification
+ [ { iterator-guard "==>" pred } ]; \hspace{-10mm} univ. iterator quantification
| [ { "\exists" binders ";" } ];
- [ { iterator-guard "&&" pred } ] ; exist. iterator quantification
- | [ { "\forall" binders ";" pred } ]; univ. quantification
- | [ { "\exists" binders ";" pred } ]; exist. quantification
- | id ":" pred ; syntactic naming
- | string ":" pred ; syntactic naming
+ [ { iterator-guard "&&" pred } ] ; \hspace{-10mm} exist. iterator quantification
+ | [ { "\forall" binders ";" pred } ]; \hspace{-10mm} univ. quantification
+ | [ { "\exists" binders ";" pred } ]; \hspace{-10mm} exist. quantification
+ | id ":" pred ; \hspace{-10mm} syntactic naming
+ | string ":" pred ; \hspace{-10mm} syntactic naming
\
[ integer-guards ] ::= [ interv ("&&" interv)* ]
\
--
GitLab