diff --git a/tests/syntax/ghost_local_ill_formed.i b/tests/syntax/ghost_local_ill_formed.i new file mode 100644 index 0000000000000000000000000000000000000000..964f39e9080b1b48322ced91f4e64b08284ff3fb --- /dev/null +++ b/tests/syntax/ghost_local_ill_formed.i @@ -0,0 +1,12 @@ +void titi() { + int c = 0; + L0: ; + /* ill-formed: in ghost mode, we have two local c in the same scope. */ + /*@ ghost int c = 1; */ + L1: ; + c = 2; + /*@ assert c == 1; */ + /*@ assert \at(c,L0) == 0; */ + /*@ assert \at(c,L1) == 1; */ + /*@ assert c == 2; */ +} diff --git a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..7e293cd87e770fb0adfaf4233fed392b3654648e --- /dev/null +++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle @@ -0,0 +1,6 @@ +[kernel] Parsing tests/syntax/ghost_local_ill_formed.i (no preprocessing) +[kernel] tests/syntax/ghost_local_ill_formed.i:5: User Error: + redefinition of 'c' in the same scope. + Previous declaration was at tests/syntax/ghost_local_ill_formed.i:2 +[kernel] User Error: stopping on file "tests/syntax/ghost_local_ill_formed.i" that has errors. +[kernel] Frama-C aborted: invalid user input.