From bd1fc51a6b63130d66c2cde1e2594c5e5802f1d8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Feb 2019 17:16:41 +0100
Subject: [PATCH] [tests] tests for new semantics of `\at` wrt local variables

---
 tests/spec/at.c                 | 29 ++++++++++++++++++++++++++
 tests/spec/oracle/at.res.oracle | 36 +++++++++++++++++++++++++++++++++
 2 files changed, 65 insertions(+)

diff --git a/tests/spec/at.c b/tests/spec/at.c
index b18cc464836..9be4a3153eb 100644
--- a/tests/spec/at.c
+++ b/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"
diff --git a/tests/spec/oracle/at.res.oracle b/tests/spec/oracle/at.res.oracle
index 31284982e1e..8194269ad90 100644
--- a/tests/spec/oracle/at.res.oracle
+++ b/tests/spec/oracle/at.res.oracle
@@ -1,4 +1,12 @@
 [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;
+}
+
 
-- 
GitLab