diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index cb8e8731d9..da14dfff1d 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -772,7 +772,7 @@ struct
       PCU.RH.replace results ctx.node new_value;
     end;
     WideningTokens.with_local_side_tokens (fun () ->
-        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
+        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
       )
 
   let init marshal =
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index ff771e692e..15df394d54 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -36,7 +36,7 @@ module type S =
     val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
     val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
 
-    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t
+    val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> relation_components_t
 
     val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> EscapeDomain.EscapedVars.t -> relation_components_t
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t
@@ -113,10 +113,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation () ->
+    | `JoinCall _ when ConfCheck.branched_thread_creation () ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread
@@ -385,10 +385,10 @@ struct
       end
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread ->
@@ -674,10 +674,10 @@ struct
       end
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread ->
@@ -1230,10 +1230,10 @@ struct
     | `Return -> st (* TODO: implement? *)
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Normal
     | `Init
     | `Thread ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a69b3a2b23..a1f0b3b08f 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -453,7 +453,7 @@ struct
     else
       ctx.local
 
-  let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ctx
+  let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread]) ctx
 
   let publish_all ctx reason =
     ignore (sync' reason ctx)
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 08413d54b1..946b8f8cc5 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -31,7 +31,7 @@ sig
   val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
   val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
 
-  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t
+  val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseComponents (D).t
 
   val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t
   val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t
@@ -322,10 +322,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Return
     | `Normal
     | `Init
@@ -433,10 +433,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Return
     | `Normal
     | `Init
@@ -802,10 +802,10 @@ struct
     match reason with
     | `Join when ConfCheck.branched_thread_creation () ->
       branched_sync ()
-    | `JoinCall when ConfCheck.branched_thread_creation_at_call ask ->
+    | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f ->
       branched_sync ()
     | `Join
-    | `JoinCall
+    | `JoinCall _
     | `Return
     | `Normal
     | `Init
@@ -1055,7 +1055,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1111,7 +1111,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1183,7 +1183,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1342,7 +1342,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1521,7 +1521,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
@@ -1704,7 +1704,7 @@ struct
     | `Return
     | `Normal
     | `Join (* TODO: no problem with branched thread creation here? *)
-    | `JoinCall
+    | `JoinCall _
     | `Init
     | `Thread ->
       st
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
index 40e50c2a69..edcf70ec98 100644
--- a/src/analyses/basePriv.mli
+++ b/src/analyses/basePriv.mli
@@ -20,7 +20,7 @@ sig
   val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
   val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
 
-  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
+  val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
 
   val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t
   val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 003cdfa96c..915b3da063 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -61,7 +61,7 @@ struct
       true
 
   (** Whether branched thread creation at start nodes of procedures needs to be handled by [sync `JoinCall] of privatization. *)
-  let branched_thread_creation_at_call (ask:Queries.ask) =
+  let branched_thread_creation_at_call (ask:Queries.ask) f =
     let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in
     if threadflag_active then
       let sens = GobConfig.get_string_list "ana.ctx_sens" in
@@ -74,7 +74,7 @@ struct
       if not threadflag_ctx_sens then
         true
       else
-        ask.f (Queries.GasExhausted)
+        ask.f (Queries.GasExhausted f)
     else
       true
 end
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index e4c0e261e4..6212b6de90 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -318,10 +318,10 @@ struct
              f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *)
           | Queries.DYojson ->
             `Lifted (D.to_yojson ctx.local)
-          | Queries.GasExhausted ->
+          | Queries.GasExhausted f ->
             if (get_int "ana.context.gas_value" >= 0) then
               (* There is a lifter above this that will answer it, save to ask *)
-              ctx.ask (Queries.GasExhausted)
+              ctx.ask (Queries.GasExhausted f)
             else
               (* Abort to avoid infinite recursion *)
               false
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 5fbb244874..b0ede0cfbf 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -124,9 +124,9 @@ type _ t =
   | MustTermLoop: stmt -> MustBool.t t
   | MustTermAllLoops: MustBool.t t
   | IsEverMultiThreaded: MayBool.t t
-  | TmpSpecial:  Mval.Exp.t -> ML.t t
+  | TmpSpecial: Mval.Exp.t -> ML.t t
   | MaySignedOverflow: exp -> MayBool.t t
-  | GasExhausted: MustBool.t t
+  | GasExhausted: CilType.Fundec.t ->  MustBool.t t
 
 type 'a result = 'a
 
@@ -197,7 +197,7 @@ struct
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
     | MaySignedOverflow  _ -> (module MayBool)
-    | GasExhausted -> (module MustBool)
+    | GasExhausted _ -> (module MustBool)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -267,7 +267,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MaySignedOverflow _ -> MayBool.top ()
-    | GasExhausted -> MustBool.top ()
+    | GasExhausted _ -> MustBool.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -334,7 +334,7 @@ struct
     | Any (TmpSpecial _) -> 56
     | Any (IsAllocVar _) -> 57
     | Any (MaySignedOverflow _) -> 58
-    | Any GasExhausted -> 59
+    | Any (GasExhausted _) -> 59
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -389,6 +389,7 @@ struct
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
       | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
+      | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
@@ -431,6 +432,7 @@ struct
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
     | Any (MaySignedOverflow e) -> CilType.Exp.hash e
+    | Any (GasExhausted f) -> CilType.Fundec.hash f
     (* IterSysVars:                                                                    *)
     (*   - argument is a function and functions cannot be compared in any meaningful way. *)
     (*   - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
@@ -494,7 +496,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
-    | Any GasExhausted -> Pretty.dprintf "GasExhausted"
+    | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
 end
 
 let to_value_domain_ask (ask: ask) =
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 717507802f..bb494382d7 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -208,7 +208,7 @@ sig
   val context: (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t
   val startcontext: unit -> C.t
 
-  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall | `Return] -> D.t
+  val sync  : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return] -> D.t
   val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result
 
   (** A transfer function which handles the assignment of a rval to a lval, i.e.,
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index ce10393d06..b1c3919bd4 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -516,7 +516,6 @@ module type Gas = sig
   module M:Lattice.S
   val startgas: unit -> M.t
   val is_exhausted: fundec -> M.t -> bool
-  val is_any_exhausted: M.t -> bool
   val callee_gas: fundec -> M.t -> M.t
   val thread_gas: varinfo -> M.t -> M.t
 end
@@ -525,7 +524,6 @@ module GlobalGas(GasVal:GasVal):Gas = struct
   module M = Lattice.Chain (struct include GasVal let names x = Format.asprintf "%d" x end)
   let startgas () = M.top () (*  get_int "ana.context.gas_value" *)
 
-  let is_any_exhausted v = v <= 0
   let is_exhausted _  = is_any_exhausted
 
   (* callee gas = caller gas - 1 *)
@@ -538,7 +536,6 @@ module PerFunctionGas(GasVal:GasVal):Gas = struct
   module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
   let startgas () = M.empty ()
   let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
-  let is_any_exhausted v = M.exists (fun _ g -> g <=0) v
   let callee_gas f v =
     let c = Option.default (G.top ()) (M.find_opt f v) in
     M.add f (max 0 c-1) v
@@ -613,10 +610,10 @@ struct
 
   let query ctx (type a) (q: a Queries.t):a Queries.result =
     match q with
-    | Queries.GasExhausted ->
+    | Queries.GasExhausted f ->
       (* The query is only used in a way where overapproximating gas exhaustion is not harmful *)
       let (d,i) = ctx.local in
-      Gas.is_any_exhausted i
+      Gas.is_exhausted f i
     | _ -> S.query (conv ctx) q
 
   let sync ctx reason                             = S.sync (conv ctx) reason, cg_val ctx
@@ -669,8 +666,8 @@ struct
     match ctx.prev_node, Cfg.prev ctx.prev_node with
     | _, _ :: _ :: _ -> (* Join in CFG. *)
       S.sync ctx `Join
-    | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
-      S.sync ctx `JoinCall
+    | FunctionEntry f, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+      S.sync ctx (`JoinCall f)
     | _, _ -> S.sync ctx `Normal
 
   let side_context sideg f c =