Handle top thread when handling thread joins in base

goblint · Oct 29, 2023 · 894e618 · 894e618
1 parent ae7a406
commit 894e618
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2372,6 +2372,7 @@ struct
         | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
         | Address ret_a ->
           begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
+            | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
             | Thread a ->
               let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in
               (* TODO: is this type right? *)