[eacsl] Add test cases for `\at` translation

src/plugins/e-acsl/tests/arith/at.i

@@ -4,7 +4,11 @@
 
 int A = 0;
 
-/*@ ensures \at(A,Post) == 3; */
+/*@
+  requires \at(A,Here) == 0;
+  requires \at(A,Pre) == 0;
+  ensures \at(A,Pre) == \at(A,Old) == 0;
+  ensures \at(A,Post) == 4; */
 void f(void) {
   A = 1;
 F:
@@ -14,6 +18,12 @@ F:
   /*@ assert \at(A,Here) == 2; */
   /*@ assert \at(\at(A,Pre),F) == 0; */
   A = 3;
+  /*@ requires \at(A,Here) == 3;
+      ensures \at(A,Pre) == 0;
+      ensures \at(A,Old) == 3;
+      ensures \at(A,Post) == 4;
+  */
+  A = 4;
 }
 
 void g(int *p, int *q) {
@@ -30,8 +40,8 @@ L2:
 L3:
   /*@ assert (\at(*(p+\at(*q,L1)),Here) == 2); */
 
-  //  /*@ assert (\at(*(p+\at(*q,L1)),L3) == 2); */ // doesn't work yet
-  //  /*@ assert (\at(*(p+\at(*q,L2)),L1)) == 1; */
+  /*@ assert (\at(*(p+\at(*q,L1)),L3) == 2); */
+  /* @ assert (\at(*(p+\at(*q,L2)),L1)) == 1; */ // should be an error
   return;
 }
 
@@ -40,6 +50,19 @@ int h(int x) {
   return x;
 }
 
+void i() {
+  // Check that \old() used in two different statements in the same function is
+  // correctly translated into two different variables
+
+  int a = 0;
+
+  /*@ ensures \old(a) + 1 == \at(a, Post); */
+  ++a;
+
+  /*@ ensures \old(a) + 1 == \at(a, Post); */
+  ++a;
+}
+
 int main(void) {
 
   int x;
@@ -58,5 +81,7 @@ L: /*@ assert x == 0; */
   int t[2];
   g(t, &x);
 
+  i();
+
   return 0;
 }

src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c

@@ -43,7 +43,7 @@ G:;
   /*@ assert
       \exists integer u; 9 <= u < 21 &&
       \forall integer v; -5 < v <= (u < 15 ? u + 6 : 3) ==>
-        \at(n + u + v > 0, K); */
+        \at(n + u + v, K) > 0; */
   ;
 
   // Function calls: