From 604c58209bf423863bbf43e7867ac1711a77687e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 23 Oct 2019 19:52:59 +0200
Subject: [PATCH] [tests] preliminary work for fixing alpha-conversion of
 locals

if a non-ghost local shadows a ghost one, the renaming should affect
the ghost.
---
 tests/syntax/ghost_local_capture.i               | 13 +++++++++++++
 .../syntax/oracle/ghost_local_capture.res.oracle | 16 ++++++++++++++++
 2 files changed, 29 insertions(+)

diff --git a/tests/syntax/ghost_local_capture.i b/tests/syntax/ghost_local_capture.i
index fc4ec789d44..32c520c6903 100644
--- a/tests/syntax/ghost_local_capture.i
+++ b/tests/syntax/ghost_local_capture.i
@@ -11,5 +11,18 @@ void titi() {
   /*@ assert c == 2; */
 }
 
+void toto() {
+  /*@ ghost int c = 1; */ {
+  L0: ;
+    int c = 0;
+  L1: ;
+    c = 2;
+    /*@ assert c == 2; */
+    /*@ assert \at(c,L0) == 1; */
+    /*@ assert \at(c,L1) == 0; */
+  }
+  /*@ assert c == 1; */
+}
+
 /*@ ghost int x; */
 /*@ ghost void f() { x++; } */
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index 6cb26bb5917..648e40245cd 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -16,6 +16,22 @@ void titi(void)
   return;
 }
 
+void toto(void)
+{
+  /*@ ghost int c = 1; */
+  {
+    L0: ;
+    int c_0 = 0;
+    L1: ;
+    c_0 = 2;
+    /*@ assert c_0 ≡ 2; */ ;
+    /*@ assert \at(c,L0) ≡ 1; */ ;
+    /*@ assert \at(c_0,L1) ≡ 0; */ ;
+  }
+  /*@ assert c ≡ 1; */ ;
+  return;
+}
+
 /*@ ghost int x; */
 /*@ ghost void f(void)
           {
-- 
GitLab