From a7ac71086ba457febc7b3bdc8a92d11ee14018c3 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Wed, 3 Oct 2018 17:26:13 +0200
Subject: [PATCH] Addresses Julien's review on the doc: - BTS #!1354 is
actually not yet fixed - Logic functions and logic global variables are not
yet supported - Better description of features that are not yet implemented -
Add missing \cinput files
---
src/plugins/e-acsl/doc/Changelog | 1 -
.../e-acsl/doc/refman/at_on-purely-logic-variables.c | 12 ++++++++++++
.../refman/at_on-purely-logic-variables_not-yet.c | 2 ++
src/plugins/e-acsl/doc/refman/speclang_modern.tex | 10 +++++-----
4 files changed, 19 insertions(+), 6 deletions(-)
create mode 100644 src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
create mode 100644 src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 5780a467c29..4adf3772d04 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -20,7 +20,6 @@
###############################################################################
-* E-ACSL [2018/10/04] Support for \at on purely logic variables.
- Fix bug #2354 about undeclared variables when using \at.
Fix bug #1762 about out-of-scope variables when using \old.
* E-ACSL [2018/10/02] Fix bug #2305 about taking the address of a
bitfield.
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
new file mode 100644
index 00000000000..88bbc974a19
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
@@ -0,0 +1,12 @@
+main(void) {
+ int m = 2;
+ int n = 7;;
+ K: ;
+ n = 875;
+ /*@ assert
+ \let k = 3;
+ \exists integer u; 9 <= u < 21 &&
+ \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
+ \at(n + u + v > 0, K); */ ;
+ 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
new file mode 100644
index 00000000000..dff4da97bd3
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
@@ -0,0 +1,2 @@
+/*@ ensures \forall int i; 0 <= i < n-1 ==> \old(t[i]) == t[i+1]; */
+void reverse(int *t, int n) { }
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index b7213239b47..3adb89eb13d 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -523,14 +523,14 @@ The \verb|\at| construct of the following example is supported.
\begin{notimplementedenv}
-However, quantified variables and let-binded variables that use C variables in
-their definition are not yet supported. Also, uses of formal variables of
-logic functions and global logic variables are not yet supported.
+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 let-binded variable \verb|w| uses C variables, namely \verb|m| and
-\verb|n|, in its definition.
+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}
--
GitLab