Handling escape event in varEq

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

tests/regression/06-symbeq/42-vareq_escape.c

@@ -0,0 +1,25 @@
+//PARAM: --set ana.activated[+] var_eq
+#include <goblint.h>
+#include <pthread.h>
+#include <unistd.h>
+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);
+}