From 2dc461af3f80195e7531233dc570dbf5eb31c5cd Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Wed, 3 Oct 2018 13:50:48 +0200
Subject: [PATCH] Changelog. Refman. Minor modif in test: unused lv.
---
src/plugins/e-acsl/doc/Changelog | 3 +++
.../e-acsl/doc/refman/changes_modern.tex | 2 ++
.../e-acsl/doc/refman/speclang_modern.tex | 24 +++++++++++++++++++
.../tests/gmp/at_on-purely-logic-variables.c | 2 +-
.../oracle/gen_at_on-purely-logic-variables.c | 6 ++---
.../gen_at_on-purely-logic-variables2.c | 2 +-
6 files changed, 34 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 21e6f600370..5780a467c29 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,9 @@
# configure configure
###############################################################################
+-* 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.
- E-ACSL [2018/09/18] Support for ranges in memory builtins
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 99a5c9360d6..bbcf78dedeb 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -119,6 +119,8 @@ in \lstinline|\\at|}
\subsection*{Version \eacslversion}
\begin{itemize}
+\item \changeinsection{at}{support of \lstinline|\\at| on purely
+logic variables}
\item \changeinsection{locations}{support of ranges in memory built-ins
(e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
\end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 2b4fa7dec49..b7213239b47 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -512,6 +512,30 @@ only the first one is accepted and valid in \eacsl since evaluating the term
\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}
+
+\end{example}
+
+
+\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.
+
+\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.
+\cinput{at_on-purely-logic-variables_not-yet.c}
+
+\end{example}
+\end{notimplementedenv}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Statement contracts}
diff --git a/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
index ef6ee47e377..a289de1d5a1 100644
--- a/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
@@ -42,7 +42,7 @@ int main(void) {
/*@ assert
\exists integer u; 9 <= u < 21 &&
\forall integer v; -5 < v <= (u < 15 ? u + 6 : 3) ==>
- \at(n + u + n > 0, K); */ ;
+ \at(n + u + v > 0, K); */ ;
// Function calls:
int t[5] = {9, 12, 12, 12, -4};
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
index e60a352da3b..c6f65b06f7c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
@@ -182,7 +182,7 @@ int main(void)
if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
}
*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) =
- (n + (long)__gen_e_acsl_u_4) + n > 0L;
+ (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_4 > 0L;
__gen_e_acsl_v_4 ++;
}
__gen_e_acsl_u_4 ++;
@@ -405,7 +405,7 @@ int main(void)
/*@ assert
∃ ℤ u;
9 ≤ u < 21 ∧
- (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + n > 0,K));
+ (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
*/
{
int __gen_e_acsl_exists_4;
@@ -468,7 +468,7 @@ int main(void)
}
e_acsl_end_loop7: ;
__e_acsl_assert(__gen_e_acsl_exists_4,(char *)"Assertion",(char *)"main",
- (char *)"\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + n > 0,K))",
+ (char *)"\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
43);
}
int t[5] = {9, 12, 12, 12, -4};
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
index 771df194b25..2c6d212d7a8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
@@ -57,7 +57,7 @@ int main(void)
assert
∃ ℤ u;
9 ≤ u < 21 ∧
- (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + n > 0,K));
+ (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
*/
;
int t[5] = {9, 12, 12, 12, -4};
--
GitLab