From d23c315b856168ac9bf3f4ee55b7d647130ec416 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 9 Oct 2019 19:13:22 +0200
Subject: [PATCH] add test case for 2421

---
 tests/syntax/ghost_local_capture.i                 |  7 +++++++
 tests/syntax/oracle/ghost_local_capture.res.oracle | 14 ++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 tests/syntax/ghost_local_capture.i
 create mode 100644 tests/syntax/oracle/ghost_local_capture.res.oracle

diff --git a/tests/syntax/ghost_local_capture.i b/tests/syntax/ghost_local_capture.i
new file mode 100644
index 00000000000..9a7ab842572
--- /dev/null
+++ b/tests/syntax/ghost_local_capture.i
@@ -0,0 +1,7 @@
+void titi() {
+  int c = 0; {
+    /*@ ghost int c = 1; */
+    c = 2;
+  }
+  /*@ assert c == 2; */
+}
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
new file mode 100644
index 00000000000..1d26a1e2767
--- /dev/null
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_local_capture.i (no preprocessing)
+/* Generated by Frama-C */
+void titi(void)
+{
+  int c = 0;
+  {
+    /*@ ghost int c_0 = 1; */
+    c_0 = 2;
+  }
+  /*@ assert c ≡ 2; */ ;
+  return;
+}
+
+
-- 
GitLab