[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

@@ -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++; } */

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)
           {