From 585a65decbf38ddfdc66ce3c544547b47877b274 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Wed, 22 Nov 2023 11:13:04 +0100
Subject: [PATCH] Check in TheadAnalysis.return whether the return is actually
 a threadreturn before side-effecting.

---
 src/analyses/threadAnalysis.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index d9140dbb37..01c5dd87fa 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -22,12 +22,15 @@ struct
   module P = IdentityP (D)
 
   (* transfer functions *)
-  let return ctx (exp:exp option) _ : D.t =
+  let handle_thread_return ctx (exp: exp option) =
     let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
-    begin match tid with
+    match tid with
       | `Lifted tid -> ctx.sideg tid (false, TS.bot (), not (D.is_empty ctx.local))
       | _ -> ()
-    end;
+
+  let return ctx (exp:exp option) _ : D.t =
+    if ctx.ask Queries.MayBeThreadReturn then
+      handle_thread_return ctx exp;
     ctx.local
 
   let rec is_not_unique ctx tid =
@@ -65,7 +68,8 @@ struct
        | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)
        | exception SetDomain.Unsupported _ -> ctx.local)
     | ThreadExit { ret_val } ->
-      return ctx (Some ret_val) ()
+      handle_thread_return ctx (Some ret_val);
+      ctx.local
     | _ -> ctx.local
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =