diff --git a/tests/basic/ghost_extern_c.cpp b/tests/basic/ghost_extern_c.cpp new file mode 100644 index 0000000000000000000000000000000000000000..dd4755356bb4b9a14bbfc115f525d44ab61741d1 --- /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 0000000000000000000000000000000000000000..ebaeee7555d45ec3478dfbf4ce11919453abae92 --- /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; + */ +