From 221601aad9b6534182eea2cacd21eae5c5fe60bd Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 31 Mar 2021 15:01:23 +0200
Subject: [PATCH] [eacsl] Update reference manual
---
src/plugins/e-acsl/doc/refman/intro_modern.tex | 1 -
src/plugins/e-acsl/doc/refman/loops.tex | 6 +++---
2 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index a8514fc0dd9..4e85af395ce 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -61,7 +61,6 @@ currently implemented into the \framac's \eacsl plug-in.
annotations
& behavior-specific annotations \\
& loop assigns \\
- & loop variants \\
& global annotations
\\
\hline
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 1de09ce3a63..f9e3599b0b7 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -11,7 +11,7 @@
\
loop-annot ::= loop-clause* ;
{ loop-behavior* } ;
- { loop-variant? }
+ loop-variant?
\
loop-clause ::= loop-invariant ;
| { loop-assigns }
@@ -23,6 +23,6 @@
{ loop-behavior } ::= { "for" id ("," id)* ":" } ;
{ loop-clause* } ; \hspace{-35mm} annotation for behavior $id$
\
- { loop-variant } ::= { "loop" "variant" term ";" } ;
- | { "loop" "variant" term "for" id ";" } ; \hspace{-35mm} variant for relation $id$
+ loop-variant ::= "loop" "variant" term ";" ;
+ | "loop" "variant" term "for" id ";" ; \hspace{-35mm} variant for relation $id$
\end{syntax}
--
GitLab