From 2a1228223481a4050bc78ba840e26415e1ff2a6d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 8 Feb 2024 17:43:36 +0100
Subject: [PATCH] update oracles

---
 tests/basic/oracle/cxx_c_link.res.oracle     | 17 +++++++++++++++++
 tests/basic/oracle/ghost_extern_c.res.oracle |  4 ++--
 2 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 tests/basic/oracle/cxx_c_link.res.oracle

diff --git a/tests/basic/oracle/cxx_c_link.res.oracle b/tests/basic/oracle/cxx_c_link.res.oracle
new file mode 100644
index 00000000..ffe2f12f
--- /dev/null
+++ b/tests/basic/oracle/cxx_c_link.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing cxx_c_link.cpp (external front-end)
+Now output intermediate result
+[kernel] Parsing cxx_c_link.c (with preprocessing)
+/* Generated by Frama-C */
+#include "__fc_alloc_axiomatic.h"
+/*@
+axiomatic dynamic_allocation {
+  predicate is_allocable{L}(ℤ n) 
+    reads __fc_heap_status;
+  
+  axiom never_allocable{L}:
+    ∀ ℤ i; i < 0 ∨ i > 18446744073709551615UL ⇒ ¬is_allocable(i);
+  
+  }
+
+*/
+
diff --git a/tests/basic/oracle/ghost_extern_c.res.oracle b/tests/basic/oracle/ghost_extern_c.res.oracle
index ebaeee75..a82f884e 100644
--- a/tests/basic/oracle/ghost_extern_c.res.oracle
+++ b/tests/basic/oracle/ghost_extern_c.res.oracle
@@ -1,8 +1,8 @@
 [kernel] Parsing ghost_extern_c.cpp (external front-end)
 Now output intermediate result
 /* Generated by Frama-C */
-/*@ ghost int _Z7ghost_x; */
+/*@ ghost int ghost_x; */
 int real_x;
-/*@ lemma sync{L}: _Z7ghost_x ≡ real_x;
+/*@ lemma sync{L}: ghost_x ≡ real_x;
  */
 
-- 
GitLab