Skip to content
Snippets Groups Projects
Commit 19475eec authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Allan Blanchard
Browse files

[tests] checks that typing reject prog with two locals with same name and scope

even if one is ghost and the other non-ghost
parent 54bb4ac6
No related branches found
No related tags found
No related merge requests found
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; */
}
[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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment