From 894e6189dfa5a27dbb0872d5feeae23e35568888 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Sun, 29 Oct 2023 21:20:47 +0200 Subject: [PATCH] Handle top thread when handling thread joins in base --- src/analyses/base.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 6536a9c496..58ab2dc219 100644 --- 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? *)