diff --git a/tests/syntax/ghost_local_capture.i b/tests/syntax/ghost_local_capture.i new file mode 100644 index 0000000000000000000000000000000000000000..9a7ab842572e9687dfef9c2b89939b02f375acd9 --- /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 0000000000000000000000000000000000000000..1d26a1e2767fb44311cb5732a3ee0a8b52f64ede --- /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; +} + +