Add TODO about shallow ThreadJoin invalidate

goblint · Dec 8, 2023 · 54bcf60 · 54bcf60
1 parent c1153a3
commit 54bcf60
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2397,6 +2397,7 @@ struct
     (* handling thread joins... sort of *)
     | ThreadJoin { thread = id; ret_var }, _ ->
       let st' =
+        (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
         match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with
         | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
         | Address ret_a ->