Skip to content
Snippets Groups Projects
Commit 086227c2 authored by Virgile Prevosto's avatar Virgile Prevosto Committed by David Bühler
Browse files

[filecheck] don't delay adding defined locals to set of known vars

they can appear before their `Local_init`, e.g. in a `SizeOfE` in the
size expression of a local array. Furthermore, we weren't really checking that
declared locals weren't used before the block in which they were supposed to
appear.
parent 4dbafc58
No related branches found
No related tags found
No related merge requests found
......@@ -132,10 +132,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
(check_abort "variables %s and %s have the same id (%d)"
v.vname v'.vname v.vid))
else
if v.vformal || v.vglob || not v.vdefined then
(* A defined local will only enter scope when the corresponding
Local_init statement is reached. *)
Varinfo.Hashtbl.add known_vars v v;
Varinfo.Hashtbl.add known_vars v v;
match v.vlogic_var_assoc with
| None -> Cil.DoChildren
| Some ({ lv_origin = Some v'} as lv) when v == v' ->
......
......@@ -16,6 +16,14 @@ void f(void)
return;
}
void h(int i)
{
int t[(unsigned int)100 / sizeof(x)];
int u[(unsigned int)100 / sizeof(i)];
int x = 1;
return;
}
int c;
int g(void)
{
......
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