From b1dc329e75e852a3d5618436bc2451caa53e142c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 11 Oct 2019 13:30:04 +0200
Subject: [PATCH] [tests] add access to ghost variable under at to show typing
 issue

---
 tests/syntax/ghost_local_capture.i                 | 5 +++++
 tests/syntax/oracle/ghost_local_capture.res.oracle | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/tests/syntax/ghost_local_capture.i b/tests/syntax/ghost_local_capture.i
index 9a7ab842572..4266c87b9c4 100644
--- a/tests/syntax/ghost_local_capture.i
+++ b/tests/syntax/ghost_local_capture.i
@@ -1,7 +1,12 @@
 void titi() {
   int c = 0; {
+    L0: ;
     /*@ ghost int c = 1; */
+    L1: ;
     c = 2;
+    /*@ assert c == 1; */
+    /*@ assert \at(c,L0) == 0; */
+    /*@ assert \at(c,L1) == 1; */
   }
   /*@ assert c == 2; */
 }
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index c6d9891d8b5..28e38a724bb 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -4,8 +4,13 @@ void titi(void)
 {
   int c = 0;
   {
+    L0: ;
     /*@ ghost int c_0 = 1; */
+    L1: ;
     c = 2;
+    /*@ assert c_0 ≡ 1; */ ;
+    /*@ assert \at(c,L0) ≡ 0; */ ;
+    /*@ assert \at(c,L1) ≡ 1; */ ;
   }
   /*@ assert c ≡ 2; */ ;
   return;
-- 
GitLab