From b316aae0934820a318e39975059e7a8c2680f26c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 8 Feb 2024 16:01:00 +0100
Subject: [PATCH] test for ghost extern c issue
---
tests/basic/ghost_extern_c.cpp | 9 +++++++++
tests/basic/oracle/ghost_extern_c.res.oracle | 8 ++++++++
2 files changed, 17 insertions(+)
create mode 100644 tests/basic/ghost_extern_c.cpp
create mode 100644 tests/basic/oracle/ghost_extern_c.res.oracle
diff --git a/tests/basic/ghost_extern_c.cpp b/tests/basic/ghost_extern_c.cpp
new file mode 100644
index 00000000..dd475535
--- /dev/null
+++ b/tests/basic/ghost_extern_c.cpp
@@ -0,0 +1,9 @@
+/* run.config
+ OPT: -cxx-unmangling=none -print
+*/
+extern "C" {
+ /*@ ghost int ghost_x; */
+ int real_x;
+
+ /*@ lemma sync: ghost_x == real_x; */
+}
diff --git a/tests/basic/oracle/ghost_extern_c.res.oracle b/tests/basic/oracle/ghost_extern_c.res.oracle
new file mode 100644
index 00000000..ebaeee75
--- /dev/null
+++ b/tests/basic/oracle/ghost_extern_c.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing ghost_extern_c.cpp (external front-end)
+Now output intermediate result
+/* Generated by Frama-C */
+/*@ ghost int _Z7ghost_x; */
+int real_x;
+/*@ lemma sync{L}: _Z7ghost_x 鈮� real_x;
+ */
+
--
GitLab