diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index fb77f0d511..740ee1dfd4 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -558,6 +558,15 @@ struct |> List.fold_left (fun st lv -> remove (Analyses.ask_of_ctx ctx) lv st ) ctx.local + | Events.Escape vars -> + if EscapeDomain.EscapedVars.is_top vars then + D.top () + else + let ask = Analyses.ask_of_ctx ctx in + let remove_var st v = + remove ask (Cil.var v) st + in + List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars) | _ -> ctx.local end diff --git a/tests/regression/06-symbeq/42-vareq_escape.c b/tests/regression/06-symbeq/42-vareq_escape.c new file mode 100644 index 0000000000..e203c7d9a1 --- /dev/null +++ b/tests/regression/06-symbeq/42-vareq_escape.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.activated[+] var_eq +#include +#include +#include +int g; + +void *t_fun1(void *arg) { + int** ptrptr = (int**) arg; + int* iptr = *ptrptr; + + *iptr = 12; +} + +int main() { + pthread_t id1; + int z = 8; + int i; + int* zptr = &z; + + int j = i; + pthread_create(&id1, NULL, t_fun1, &zptr); + zptr = &i; + __goblint_check(i == j); //UNKNOWN! + pthread_join (id1, NULL); +} \ No newline at end of file