Add commented out possible fix to unsound var_eq invalidate

goblint · Mar 1, 2022 · 73cd135 · 73cd135
1 parent d239760
commit 73cd135
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
@@ -402,7 +402,10 @@ struct
       | None -> None
       | Some st ->
         let vs = ask.f (Queries.ReachableFrom e) in
-        Some (Queries.LS.join vs st)
+        if Queries.LS.is_top vs then
+          None
+        else
+          Some (Queries.LS.join vs st)
     in
     List.fold_right reachable es (Some (Queries.LS.empty ()))
 
@@ -496,6 +499,8 @@ struct
         D.B.fold remove_reachable2 es st
       in
       D.fold remove_reachable1 ctx.local ctx.local
+      (* TODO: do something like this instead to be sound? *)
+      (* List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs []) *)
 
   let unknown_fn ctx lval f args =
     let args =