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 0000000000000000000000000000000000000000..ffe2f12f249af89be7f8a0c2ff290b8bc3b42198 --- /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 ebaeee7555d45ec3478dfbf4ce11919453abae92..a82f884e3cb4106c390bbefdba9a06542697a0fe 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; */