[tests] tests for new semantics of `\at` wrt local variables

tests/spec/at.c

@@ -22,6 +22,35 @@ int f(int y) {
   return x;
 }
 
+void test () {
+  int x = 0;
+  L1: {
+  int x = 1;
+  L2:
+  // assert below speaks about two distinct x.
+  /*@ assert \at(&x, L1) != \at(&x,L2); */
+  x = 2;
+  }
+}
+
+void ko (int z) {
+  L: {
+    int y = 0;
+    // assert below should not typecheck: y is not in scope at L (nor at Pre)
+    //@ assert KO: \at(y,L) == 0;
+    //@ assert KO: \at(y,Pre) == 0;
+    //@ assert KO: \at(z,Init) == 0; // at Init, only globals are in scope
+    //@ assert OK: \at (x,Init) == 0;
+    //@ assert OK: \at(z,Pre) == 0;
+  }
+  while (x>0) {
+    int i = 1;
+    x--;
+    //@ assert KO: \at(i,LoopCurrent) == 1;
+    //@ assert OK: \at(z,LoopCurrent) == \at(z,Pre);
+  }
+}
+
 /*
 Local Variables:
 compile-command: "PPCHOME=../.. LC_ALL=C make at"

tests/spec/oracle/at.res.oracle

 [kernel] Parsing tests/spec/at.c (with preprocessing)
+[kernel:annot-error] tests/spec/at.c:40: Warning: 
+  unbound logic variable y. Ignoring code annotation
+[kernel:annot-error] tests/spec/at.c:41: Warning: 
+  unbound logic variable y. Ignoring code annotation
+[kernel:annot-error] tests/spec/at.c:42: Warning: 
+  unbound logic variable z. Ignoring code annotation
+[kernel:annot-error] tests/spec/at.c:49: Warning: 
+  unbound logic variable i. Ignoring code annotation
 /* Generated by Frama-C */
 int x;
 /*@
@@ -28,4 +36,32 @@ int f(int y)
   return x;
 }
 
+void test(void)
+{
+  int x_0 = 0;
+  L1:
+  {
+    int x_1 = 1;
+    L2: /*@ assert \at(&x_0,L1) ≢ \at(&x_1,L2); */ ;
+    x_1 = 2;
+  }
+  return;
+}
+
+void ko(int z)
+{
+  L:
+  {
+    int y = 0;
+    /*@ assert OK: \at(x,Init) ≡ 0; */ ;
+    /*@ assert OK: \at(z,Pre) ≡ 0; */ ;
+  }
+  while (x > 0) {
+    int i = 1;
+    x --;
+    /*@ assert OK: \at(z,LoopCurrent) ≡ \at(z,Pre); */ ;
+  }
+  return;
+}
+