Changelog. Refman. Minor modif in test: unused lv.

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

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}

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}

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

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

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