From 08d56aa0d8e6e13b1ff87fd11d3bdffc8218611a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 24 Sep 2023 16:51:17 +0200
Subject: [PATCH 01/19] Add argument to `threadenter`

---
 src/analyses/abortUnless.ml                  |  2 +-
 src/analyses/accessAnalysis.ml               |  2 +-
 src/analyses/activeLongjmp.ml                |  2 +-
 src/analyses/activeSetjmp.ml                 |  2 +-
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/expsplit.ml                     |  2 +-
 src/analyses/extractPthread.ml               |  2 +-
 src/analyses/fileUse.ml                      |  2 +-
 src/analyses/locksetAnalysis.ml              |  2 +-
 src/analyses/mCP.ml                          | 12 ++++-----
 src/analyses/mallocFresh.ml                  |  2 +-
 src/analyses/malloc_null.ml                  |  2 +-
 src/analyses/modifiedSinceLongjmp.ml         |  2 +-
 src/analyses/mutexTypeAnalysis.ml            |  2 +-
 src/analyses/poisonVariables.ml              |  2 +-
 src/analyses/pthreadSignals.ml               |  2 +-
 src/analyses/region.ml                       |  2 +-
 src/analyses/spec.ml                         |  2 +-
 src/analyses/stackTrace.ml                   |  4 +--
 src/analyses/symbLocks.ml                    |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/termination.ml                  |  2 +-
 src/analyses/threadAnalysis.ml               |  2 +-
 src/analyses/threadEscape.ml                 |  2 +-
 src/analyses/threadFlag.ml                   |  2 +-
 src/analyses/threadId.ml                     |  8 +++---
 src/analyses/threadReturn.ml                 |  2 +-
 src/analyses/tmpSpecial.ml                   |  2 +-
 src/analyses/tutorials/taint.ml              |  2 +-
 src/analyses/tutorials/unitAnalysis.ml       |  2 +-
 src/analyses/uninit.ml                       |  2 +-
 src/analyses/useAfterFree.ml                 |  4 +--
 src/analyses/varEq.ml                        |  2 +-
 src/analyses/vla.ml                          |  2 +-
 src/analyses/wrapperFunctionAnalysis.ml      |  2 +-
 src/framework/analyses.ml                    |  6 ++---
 src/framework/constraints.ml                 | 27 ++++++++++----------
 src/framework/control.ml                     |  6 ++---
 src/framework/resultQuery.ml                 |  6 ++---
 src/util/wideningTokens.ml                   |  2 +-
 src/witness/observerAnalysis.ml              |  2 +-
 src/witness/witnessConstraints.ml            |  4 +--
 44 files changed, 74 insertions(+), 73 deletions(-)

diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 813d999ac3..1c77803c7e 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -65,7 +65,7 @@ struct
     false
 
   let startstate v = false
-  let threadenter ctx lval f args = [false]
+  let threadenter ?(multiple=false) ctx lval f args = [false]
   let threadspawn ctx lval f args fctx = false
   let exitstate v = false
 end
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index e99aefa0e5..bd1ca528a7 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -54,7 +54,7 @@ struct
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ctx lval f args = [()]
+  let threadenter ?(multiple=false) ctx lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 
diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
index 9c9868e32f..43da8c6512 100644
--- a/src/analyses/activeLongjmp.ml
+++ b/src/analyses/activeLongjmp.ml
@@ -26,7 +26,7 @@ struct
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
index 069111d3ba..a69bf4db95 100644
--- a/src/analyses/activeSetjmp.ml
+++ b/src/analyses/activeSetjmp.ml
@@ -25,7 +25,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 46c620f390..d56064a42f 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -647,7 +647,7 @@ struct
 
   (* Thread transfer functions. *)
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 71e2661997..cb29cbc0ab 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2503,7 +2503,7 @@ struct
     in
     combine_one ctx.local after
 
-  let threadenter ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
+  let threadenter ?(multiple=false) ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
       [make_entry ~thread:true ctx fd args]
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 04b148dd02..3a2cc5798d 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -155,7 +155,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index f121d0380e..9c610a96bf 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -84,7 +84,7 @@ struct
     in
     emit_splits ctx d
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
 
   let threadspawn ctx lval f args fctx =
     emit_splits_ctx ctx
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 60e389fedf..591704cc70 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1238,7 +1238,7 @@ module Spec : Analyses.MCPSpec = struct
       (Ctx.top ())
 
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let d : D.t = ctx.local in
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index a9088a4bb2..b12953c71c 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -287,7 +287,7 @@ struct
     | _ -> m
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 2e9e08f03d..56fe960a47 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -18,7 +18,7 @@ struct
   module C = D
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
   let exitstate  v = D.empty ()
 end
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 1b6a7e5a1d..e305e9c7f6 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -140,9 +140,9 @@ struct
         f ((k,v::a')::a) b
     in f [] xs
 
-  let do_spawns ctx (xs:(varinfo * (lval option * exp list)) list) =
+  let do_spawns ctx (xs:(varinfo * (lval option * exp list * bool)) list) =
     let spawn_one v d =
-      List.iter (fun (lval, args) -> ctx.spawn lval v args) d
+      List.iter (fun (lval, args, multiple) -> ctx.spawn ~multiple lval v args) d
     in
     if not (get_bool "exp.single-threaded") then
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
@@ -322,8 +322,8 @@ struct
 
   and outer_ctx tfname ?spawns ?sides ?emits ctx =
     let spawn = match spawns with
-      | Some spawns -> (fun l v a  -> spawns := (v,(l,a)) :: !spawns)
-      | None -> (fun v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
+      | Some spawns -> (fun ?(multiple=false) l v a  -> spawns := (v,(l,a,multiple)) :: !spawns)
+      | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
       | Some sides -> (fun v g    -> sides  := (v, (!WideningTokens.side_tokens, g)) :: !sides)
@@ -565,13 +565,13 @@ struct
     let d = do_emits ctx !emits d q in
     if q then raise Deadcode else d
 
-  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
+  let threadenter ?(multiple=false) (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadenter" ~sides ~emits ctx in
     let f (n,(module S:MCPSpec),d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadenter" ctx'' n d in
-      map (fun d -> (n, repr d)) @@ S.threadenter ctx' lval f a
+      map (fun d -> (n, repr d)) @@ (S.threadenter ~multiple) ctx' lval f a
     in
     let css = map f @@ spec_list ctx.local in
     do_sideg ctx !sides;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 2c2b99a075..861e4958bd 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -52,7 +52,7 @@ struct
       | None -> ctx.local
       | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.empty ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 4d5871cb80..2d90112636 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -215,7 +215,7 @@ struct
   let name () = "malloc_null"
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 0375bd3f74..d9c8f5102c 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -63,7 +63,7 @@ struct
       ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 806c35f464..7051173bd0 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -65,7 +65,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 1bd4b6d544..8c79626cc9 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -61,7 +61,7 @@ struct
     VS.join au ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let event ctx e octx =
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 0b776282e8..83455965ec 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -73,7 +73,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = Signals.empty ()
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
   let exitstate  v = Signals.empty ()
 end
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 6d2ae246c3..9d68221fcd 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -175,7 +175,7 @@ struct
   let startstate v =
     `Lifted (RegMap.bot ())
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local
 
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index 54ffcd2697..e5434eb264 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -487,7 +487,7 @@ struct
 
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index 4dc62f1873..3d70c50856 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -21,7 +21,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 end
 
@@ -45,7 +45,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.top ()
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.push !Tracing.current_loc ctx.local]
 end
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index d8cebf51d2..b99ef93039 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -29,7 +29,7 @@ struct
   let name () = "symb_locks"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index d053cd103b..25e981dcbf 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -101,7 +101,7 @@ struct
     d
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.bot ()]
   let threadspawn ctx lval f args fctx =
     match lval with
diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml
index 6da9225d3f..5e5e0d36f1 100644
--- a/src/analyses/termination.ml
+++ b/src/analyses/termination.ml
@@ -217,7 +217,7 @@ struct
   (* | _ -> ctx.local *)
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 1e679a4707..26e6702c25 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -84,7 +84,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 9ed62e7422..0674ebf3d1 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -150,7 +150,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     [D.bot ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index f2ebf82be1..f3b132918a 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -58,7 +58,7 @@ struct
   let access ctx _ =
     is_currently_multi (Analyses.ask_of_ctx ctx)
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 4acf88a7ef..f1de1dfdcb 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -56,9 +56,9 @@ struct
       Hashtbl.replace !tids tid ();
     (N.bot (), `Lifted (tid), (TD.bot (), TD.bot ()))
 
-  let create_tid (_, current, (td, _)) ((node, index): Node.t * int option) v =
+  let create_tid ?(multiple=false) (_, current, (td, _)) ((node, index): Node.t * int option) v =
     match current with
-    | `Lifted current ->
+    | `Lifted current when not multiple ->
       let+ tid = Thread.threadenter (current, td) node index v in
       if GobConfig.get_bool "dbg.print_tids" then
         Hashtbl.replace !tids tid ();
@@ -133,9 +133,9 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter ctx lval f args:D.t list =
+  let threadenter ?(multiple=false) ctx lval f args:D.t list =
     let n, i = indexed_node_for_ctx ctx in
-    let+ tid = create_tid ctx.local (n, i) f in
+    let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index 470c4ceaa8..176a4d3465 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -28,7 +28,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = true
-  let threadenter ctx lval f args = [true]
+  let threadenter ?(multiple=false) ctx lval f args = [true]
   let exitstate  v = D.top ()
 
   let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index 2d38972d7a..f3d092e59e 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -88,7 +88,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 3067449e31..166ce2c3f6 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -129,7 +129,7 @@ struct
 
   (* You may leave these alone *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index d3b8c69bfd..b5fb4d6367 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -39,7 +39,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index f8759d9134..abdcd67aaa 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -25,7 +25,7 @@ struct
   let name () = "uninit"
 
   let startstate v : D.t = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 0aafbd1ad4..6033c689e1 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -196,7 +196,7 @@ struct
       end
     | _ -> state
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 
   let startstate v = D.bot ()
@@ -205,4 +205,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 634a684c7c..7bd3453b8a 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -43,7 +43,7 @@ struct
   let name () = "var_eq"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml
index 865f22b20a..8bd0168de0 100644
--- a/src/analyses/vla.ml
+++ b/src/analyses/vla.ml
@@ -33,7 +33,7 @@ struct
     ctx.local || Cilfacade.isVLAType v.vtype
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index d9bbdb6197..89242e044e 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -87,7 +87,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     (* The new thread receives a fresh counter *)
     [D.bot ()]
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index df3346af93..54a3a18f1a 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -342,7 +342,7 @@ type ('d,'g,'c,'v) ctx =
   ; edge     : MyCFG.edge
   ; local    : 'd
   ; global   : 'v -> 'g
-  ; spawn    : lval option -> varinfo -> exp list -> unit
+  ; spawn    : ?multiple:bool -> lval option -> varinfo -> exp list -> unit
   ; split    : 'd -> Events.t list -> unit
   ; sideg    : 'v -> 'g -> unit
   }
@@ -444,7 +444,7 @@ sig
   val paths_as_set : (D.t, G.t, C.t, V.t) ctx -> D.t list
 
   (** Returns initial state for created thread. *)
-  val threadenter : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
+  val threadenter : ?multiple:bool -> (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
 
   (** Updates the local state of the creator thread using initial state of created thread. *)
   val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
@@ -696,7 +696,7 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
     ctx.local
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 end
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 740d1f85a9..a7683fb6b3 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -83,8 +83,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     D.lift @@ S.combine_assign (conv ctx) r fe f args fc (D.unlift es) f_ask
 
-  let threadenter ctx lval f args =
-    List.map D.lift @@ S.threadenter (conv ctx) lval f args
+  let threadenter ?(multiple=false) ctx lval f args =
+    List.map D.lift @@ (S.threadenter ~multiple) (conv ctx) lval f args
 
   let threadspawn ctx lval f args fctx =
     D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -167,8 +167,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     S.combine_assign (conv ctx) r fe f args (Option.map C.unlift fc) es f_ask
 
-  let threadenter ctx lval f args =
-    S.threadenter (conv ctx) lval f args
+  let threadenter ?(multiple=false) ctx lval f args =
+    S.threadenter ~multiple (conv ctx) lval f args
 
   let threadspawn ctx lval f args fctx =
     S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -249,7 +249,7 @@ struct
   let combine_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
-  let threadenter ctx lval f args = lift_fun ctx (List.map lift_start_level) S.threadenter ((|>) args % (|>) f % (|>) lval)
+  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
   let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
@@ -394,7 +394,7 @@ struct
 
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
 
-  let threadenter ctx lval f args = S.threadenter (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
+  let threadenter ?(multiple=false) ctx lval f args = S.threadenter ~multiple (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
   let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let enter ctx r f args =
@@ -485,7 +485,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
-  let threadenter ctx lval f args = lift_fun ctx (List.map D.lift) S.threadenter ((|>) args % (|>) f % (|>) lval) []
+  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
   let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
 
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
@@ -581,7 +581,7 @@ struct
       ; split   = (fun (d:D.t) es -> assert (List.is_empty es); r := d::!r)
       ; sideg   = (fun g d -> sideg (GVar.spec g) (G.create_spec d))
       }
-    and spawn lval f args =
+    and spawn ?(multiple=false) lval f args =
       (* TODO: adjust ctx node/edge? *)
       (* TODO: don't repeat for all paths that spawn same *)
       let ds = S.threadenter ctx lval f args in
@@ -898,7 +898,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = S.startstate Cil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *)
       ; global = (fun g -> G.spec (getg (GVar.spec g)))
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
+      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in query context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
       }
@@ -1262,9 +1262,10 @@ struct
     let fd1 = D.choose octx.local in
     map ctx Spec.event (fun h -> h e (conv octx fd1))
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
-    fold' ctx Spec.threadenter (fun h -> h lval f args) g []
+    fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
+
   let threadspawn ctx lval f args fctx =
     let fd1 = D.choose fctx.local in
     map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))
@@ -1448,7 +1449,7 @@ struct
   let combine_env ctx = S.combine_env (conv ctx)
   let combine_assign ctx = S.combine_assign (conv ctx)
   let special ctx = S.special (conv ctx)
-  let threadenter ctx = S.threadenter (conv ctx)
+  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
@@ -1684,7 +1685,7 @@ struct
       List.iter handle_path (S.paths_as_set conv_ctx);
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
-  let threadenter ctx = S.threadenter (conv ctx)
+  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5cefc1a7de..72890be4b4 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -280,7 +280,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = Spec.D.top ()
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun _ -> failwith "Global initializers should never spawn threads. What is going on?")
+        ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
         ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -385,7 +385,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+        ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -417,7 +417,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+        ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
diff --git a/src/framework/resultQuery.ml b/src/framework/resultQuery.ml
index ce5839ef30..c676c41c14 100644
--- a/src/framework/resultQuery.ml
+++ b/src/framework/resultQuery.ml
@@ -18,7 +18,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = local
       ; global = (fun g -> try EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)) with Not_found -> Spec.G.bot ()) (* see 29/29 on why fallback is needed *)
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in witness context.")
+      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in witness context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
       }
@@ -37,7 +37,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = local
       ; global = (fun g -> try EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)) with Not_found -> Spec.G.bot ()) (* TODO: how can be missing? *)
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in witness context.")
+      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in witness context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
       }
@@ -57,7 +57,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = Spec.startstate GoblintCil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *) (* TODO: is this startstate bad? *)
       ; global = (fun v -> EQSys.G.spec (try GHT.find gh (EQSys.GVar.spec v) with Not_found -> EQSys.G.bot ())) (* TODO: how can be missing? *)
-      ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
+      ; spawn  = (fun ?(multiple=false) v d   -> failwith "Cannot \"spawn\" in query context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
       }
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 75f0e4f81d..c88f3f00c1 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -179,7 +179,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
-  let threadenter ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) S.threadenter ((|>) args % (|>) f % (|>) lval)
+  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
   let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
   let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
 end
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index c8d8563909..3c702d199f 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -76,7 +76,7 @@ struct
     step_ctx ctx
 
   let startstate v = `Lifted Automaton.initial
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 2ce16a5997..ad32713fa8 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -199,7 +199,7 @@ struct
     let r = Dom.bindings a in
     List.map (fun (x,v) -> (Dom.singleton x v, b)) r
 
-  let threadenter ctx lval f args =
+  let threadenter ?(multiple=false) ctx lval f args =
     let g xs x' ys =
       let ys' = List.map (fun y ->
           let yr = step ctx.prev_node (ctx.context ()) x' (ThreadEntry (lval, f, args)) (nosync x') in (* threadenter called on before-sync state *)
@@ -208,7 +208,7 @@ struct
       in
       ys' @ xs
     in
-    fold' ctx Spec.threadenter (fun h -> h lval f args) g []
+    fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
   let threadspawn ctx lval f args fctx =
     let fd1 = Dom.choose_key (fst fctx.local) in
     map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))

From a32513936348d54c724697aba3943c409585f46a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 24 Sep 2023 17:28:01 +0200
Subject: [PATCH 02/19] Spawn non-unique threads

---
 src/analyses/base.ml                             | 14 +++++++-------
 src/analyses/threadAnalysis.ml                   |  8 +++++++-
 src/framework/constraints.ml                     |  2 +-
 tests/regression/40-threadid/09-multiple.c       | 15 +++++++++++++++
 .../regression/40-threadid/10-multiple-thread.c  | 16 ++++++++++++++++
 5 files changed, 46 insertions(+), 9 deletions(-)
 create mode 100644 tests/regression/40-threadid/09-multiple.c
 create mode 100644 tests/regression/40-threadid/10-multiple-thread.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index cb29cbc0ab..3b6be2eff8 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1902,7 +1902,7 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list * bool =
     let create_thread lval arg v =
       try
         (* try to get function declaration *)
@@ -1943,7 +1943,7 @@ struct
           else
             start_funvars
         in
-        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
+        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
@@ -1956,9 +1956,9 @@ struct
       let deep_flist = collect_invalidate ~deep:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local deep_args in
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
-      if addrs <> [] then M.debug ~category:Analyzer "Spawning functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
-      List.filter_map (create_thread None None) addrs
-    | _, _ -> []
+      if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
+      List.filter_map (create_thread None None) addrs, true
+    | _, _ -> [], false
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2024,9 +2024,9 @@ struct
       let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
       (addr, AD.type_of addr)
     in
-    let forks = forkfun ctx lv f args in
+    let forks, multiple = forkfun ctx lv f args in
     if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple3.second forks);
-    List.iter (BatTuple.Tuple3.uncurry ctx.spawn) forks;
+    List.iter (BatTuple.Tuple3.uncurry (ctx.spawn ~multiple)) forks;
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 26e6702c25..740cca3a53 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -84,7 +84,13 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+
+  let threadenter ?(multiple=false) ctx lval f args =
+    if multiple then
+      (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
+       ctx.sideg tid (true, TS.bot (), false));
+    [D.bot ()]
+
   let threadspawn ctx lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index a7683fb6b3..62b8d46efa 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -584,7 +584,7 @@ struct
     and spawn ?(multiple=false) lval f args =
       (* TODO: adjust ctx node/edge? *)
       (* TODO: don't repeat for all paths that spawn same *)
-      let ds = S.threadenter ctx lval f args in
+      let ds = S.threadenter ~multiple ctx lval f args in
       List.iter (fun d ->
           spawns := (lval, f, args, d) :: !spawns;
           match Cilfacade.find_varinfo_fundec f with
diff --git a/tests/regression/40-threadid/09-multiple.c b/tests/regression/40-threadid/09-multiple.c
new file mode 100644
index 0000000000..5510e5ae07
--- /dev/null
+++ b/tests/regression/40-threadid/09-multiple.c
@@ -0,0 +1,15 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+int main(void) {
+  // This should spawn a non-unique thread
+  unknown(t_fun);
+  return 0;
+}
diff --git a/tests/regression/40-threadid/10-multiple-thread.c b/tests/regression/40-threadid/10-multiple-thread.c
new file mode 100644
index 0000000000..0024d268ec
--- /dev/null
+++ b/tests/regression/40-threadid/10-multiple-thread.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.activated[+] thread
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+int main(void) {
+  // This should spawn a non-unique thread
+  unknown(t_fun);
+  return 0;
+}

From ccaffc592932a7c6ca219aadc28d6f7b74188fcf Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 25 Sep 2023 13:07:31 +0200
Subject: [PATCH 03/19] Turn optional argument into named argument

---
 src/analyses/abortUnless.ml                  |  2 +-
 src/analyses/accessAnalysis.ml               |  2 +-
 src/analyses/activeLongjmp.ml                |  2 +-
 src/analyses/activeSetjmp.ml                 |  2 +-
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/expsplit.ml                     |  2 +-
 src/analyses/extractPthread.ml               |  2 +-
 src/analyses/fileUse.ml                      |  2 +-
 src/analyses/locksetAnalysis.ml              |  2 +-
 src/analyses/mCP.ml                          |  2 +-
 src/analyses/mallocFresh.ml                  |  2 +-
 src/analyses/malloc_null.ml                  |  2 +-
 src/analyses/modifiedSinceLongjmp.ml         |  2 +-
 src/analyses/mutexTypeAnalysis.ml            |  2 +-
 src/analyses/poisonVariables.ml              |  2 +-
 src/analyses/pthreadSignals.ml               |  2 +-
 src/analyses/region.ml                       |  2 +-
 src/analyses/spec.ml                         |  2 +-
 src/analyses/stackTrace.ml                   |  4 ++--
 src/analyses/symbLocks.ml                    |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/termination.ml                  |  2 +-
 src/analyses/threadAnalysis.ml               |  2 +-
 src/analyses/threadEscape.ml                 |  2 +-
 src/analyses/threadFlag.ml                   |  2 +-
 src/analyses/threadId.ml                     |  2 +-
 src/analyses/threadReturn.ml                 |  2 +-
 src/analyses/tmpSpecial.ml                   |  2 +-
 src/analyses/tutorials/taint.ml              |  2 +-
 src/analyses/tutorials/unitAnalysis.ml       |  2 +-
 src/analyses/uninit.ml                       |  2 +-
 src/analyses/useAfterFree.ml                 |  2 +-
 src/analyses/varEq.ml                        |  2 +-
 src/analyses/vla.ml                          |  2 +-
 src/analyses/wrapperFunctionAnalysis.ml      |  2 +-
 src/framework/analyses.ml                    |  4 ++--
 src/framework/constraints.ml                 | 20 ++++++++++----------
 src/framework/control.ml                     |  2 +-
 src/util/wideningTokens.ml                   |  2 +-
 src/witness/observerAnalysis.ml              |  2 +-
 src/witness/witnessConstraints.ml            |  2 +-
 43 files changed, 54 insertions(+), 54 deletions(-)

diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 1c77803c7e..5c24e61f7c 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -65,7 +65,7 @@ struct
     false
 
   let startstate v = false
-  let threadenter ?(multiple=false) ctx lval f args = [false]
+  let threadenter ctx ~multiple lval f args = [false]
   let threadspawn ctx lval f args fctx = false
   let exitstate v = false
 end
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index bd1ca528a7..f0025c2f1c 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -54,7 +54,7 @@ struct
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ?(multiple=false) ctx lval f args = [()]
+  let threadenter ctx ~multiple lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 
diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
index 43da8c6512..9baa601ddc 100644
--- a/src/analyses/activeLongjmp.ml
+++ b/src/analyses/activeLongjmp.ml
@@ -26,7 +26,7 @@ struct
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
index a69bf4db95..be13489993 100644
--- a/src/analyses/activeSetjmp.ml
+++ b/src/analyses/activeSetjmp.ml
@@ -25,7 +25,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index d56064a42f..c232ccae9b 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -647,7 +647,7 @@ struct
 
   (* Thread transfer functions. *)
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 3b6be2eff8..e824fac013 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2503,7 +2503,7 @@ struct
     in
     combine_one ctx.local after
 
-  let threadenter ?(multiple=false) ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
+  let threadenter ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list): D.t list =
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
       [make_entry ~thread:true ctx fd args]
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 3a2cc5798d..820ff69efa 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -155,7 +155,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index 9c610a96bf..141a04283b 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -84,7 +84,7 @@ struct
     in
     emit_splits ctx d
 
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
 
   let threadspawn ctx lval f args fctx =
     emit_splits_ctx ctx
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 591704cc70..f72f72c1fe 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1238,7 +1238,7 @@ module Spec : Analyses.MCPSpec = struct
       (Ctx.top ())
 
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let d : D.t = ctx.local in
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index b12953c71c..b8e7fd78f5 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -287,7 +287,7 @@ struct
     | _ -> m
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 56fe960a47..6a816b9e6c 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -18,7 +18,7 @@ struct
   module C = D
 
   let startstate v = D.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let exitstate  v = D.empty ()
 end
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index e305e9c7f6..5259bdb6c7 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -565,7 +565,7 @@ struct
     let d = do_emits ctx !emits d q in
     if q then raise Deadcode else d
 
-  let threadenter ?(multiple=false) (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
+  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) ~multiple lval f a =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadenter" ~sides ~emits ctx in
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 861e4958bd..e171ad4ea1 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -52,7 +52,7 @@ struct
       | None -> ctx.local
       | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.empty ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 2d90112636..41c251dfce 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -215,7 +215,7 @@ struct
   let name () = "malloc_null"
 
   let startstate v = D.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index d9c8f5102c..7da0030b9a 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -63,7 +63,7 @@ struct
       ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 7051173bd0..66e60aede1 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -65,7 +65,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 8c79626cc9..87dddd1e54 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -61,7 +61,7 @@ struct
     VS.join au ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let event ctx e octx =
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 83455965ec..70f1624922 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -73,7 +73,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = Signals.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let exitstate  v = Signals.empty ()
 end
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 9d68221fcd..86cad5684b 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -175,7 +175,7 @@ struct
   let startstate v =
     `Lifted (RegMap.bot ())
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local
 
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index e5434eb264..c44edd6c87 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -487,7 +487,7 @@ struct
 
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index 3d70c50856..3c3bd56640 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -21,7 +21,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 end
 
@@ -45,7 +45,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.top ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.push !Tracing.current_loc ctx.local]
 end
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index b99ef93039..32be32f73d 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -29,7 +29,7 @@ struct
   let name () = "symb_locks"
 
   let startstate v = D.top ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 25e981dcbf..b45ea54877 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -101,7 +101,7 @@ struct
     d
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.bot ()]
   let threadspawn ctx lval f args fctx =
     match lval with
diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml
index 5e5e0d36f1..0563730fb2 100644
--- a/src/analyses/termination.ml
+++ b/src/analyses/termination.ml
@@ -217,7 +217,7 @@ struct
   (* | _ -> ctx.local *)
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 740cca3a53..ff4b4d5c63 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -85,7 +85,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     if multiple then
       (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
        ctx.sideg tid (true, TS.bot (), false));
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 0674ebf3d1..0948a3976d 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -150,7 +150,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.bot ()]
 
   let threadspawn ctx lval f args fctx =
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index f3b132918a..81e05af679 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -58,7 +58,7 @@ struct
   let access ctx _ =
     is_currently_multi (Analyses.ask_of_ctx ctx)
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index f1de1dfdcb..a9f3fa35f7 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -133,7 +133,7 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter ?(multiple=false) ctx lval f args:D.t list =
+  let threadenter ctx ~multiple lval f args:D.t list =
     let n, i = indexed_node_for_ctx ctx in
     let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index 176a4d3465..0aed06851a 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -28,7 +28,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = true
-  let threadenter ?(multiple=false) ctx lval f args = [true]
+  let threadenter ctx ~multiple lval f args = [true]
   let exitstate  v = D.top ()
 
   let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index f3d092e59e..046345e627 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -88,7 +88,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 166ce2c3f6..7fc3fd7343 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -129,7 +129,7 @@ struct
 
   (* You may leave these alone *)
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index b5fb4d6367..3ecddc2bc0 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -39,7 +39,7 @@ struct
     ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index abdcd67aaa..2b388d1190 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -25,7 +25,7 @@ struct
   let name () = "uninit"
 
   let startstate v : D.t = D.empty ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 6033c689e1..0c7a46c35f 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -196,7 +196,7 @@ struct
       end
     | _ -> state
 
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 
   let startstate v = D.bot ()
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 7bd3453b8a..3aaef95265 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -43,7 +43,7 @@ struct
   let name () = "var_eq"
 
   let startstate v = D.top ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml
index 8bd0168de0..665612aa99 100644
--- a/src/analyses/vla.ml
+++ b/src/analyses/vla.ml
@@ -33,7 +33,7 @@ struct
     ctx.local || Cilfacade.isVLAType v.vtype
 
   let startstate v = D.bot ()
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index 89242e044e..a1bec69a8c 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -87,7 +87,7 @@ struct
 
   let startstate v = D.bot ()
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     (* The new thread receives a fresh counter *)
     [D.bot ()]
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 54a3a18f1a..3bb88a6ead 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -444,7 +444,7 @@ sig
   val paths_as_set : (D.t, G.t, C.t, V.t) ctx -> D.t list
 
   (** Returns initial state for created thread. *)
-  val threadenter : ?multiple:bool -> (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t list
+  val threadenter : (D.t, G.t, C.t, V.t) ctx -> multiple:bool -> lval option -> varinfo -> exp list -> D.t list
 
   (** Updates the local state of the creator thread using initial state of created thread. *)
   val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
@@ -696,7 +696,7 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
     ctx.local
 
-  let threadenter ?(multiple=false) ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let threadspawn ctx lval f args fctx = ctx.local
 end
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 62b8d46efa..ed492f4237 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -83,8 +83,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     D.lift @@ S.combine_assign (conv ctx) r fe f args fc (D.unlift es) f_ask
 
-  let threadenter ?(multiple=false) ctx lval f args =
-    List.map D.lift @@ (S.threadenter ~multiple) (conv ctx) lval f args
+  let threadenter ctx ~multiple lval f args =
+    List.map D.lift @@ S.threadenter (conv ctx) ~multiple lval f args
 
   let threadspawn ctx lval f args fctx =
     D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -167,8 +167,8 @@ struct
   let combine_assign ctx r fe f args fc es f_ask =
     S.combine_assign (conv ctx) r fe f args (Option.map C.unlift fc) es f_ask
 
-  let threadenter ?(multiple=false) ctx lval f args =
-    S.threadenter ~multiple (conv ctx) lval f args
+  let threadenter ctx ~multiple lval f args =
+    S.threadenter (conv ctx) ~multiple lval f args
 
   let threadspawn ctx lval f args fctx =
     S.threadspawn (conv ctx) lval f args (conv fctx)
@@ -249,7 +249,7 @@ struct
   let combine_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
-  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
   let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
@@ -394,7 +394,7 @@ struct
 
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
 
-  let threadenter ?(multiple=false) ctx lval f args = S.threadenter ~multiple (conv ctx) lval f args |> List.map (fun d -> (d, snd ctx.local))
+  let threadenter ctx ~multiple lval f args = S.threadenter (conv ctx) ~multiple lval f args |> List.map (fun d -> (d, snd ctx.local))
   let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let enter ctx r f args =
@@ -485,7 +485,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
-  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
   let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
 
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
@@ -1262,7 +1262,7 @@ struct
     let fd1 = D.choose octx.local in
     map ctx Spec.event (fun h -> h e (conv octx fd1))
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
     fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
 
@@ -1449,7 +1449,7 @@ struct
   let combine_env ctx = S.combine_env (conv ctx)
   let combine_assign ctx = S.combine_assign (conv ctx)
   let special ctx = S.special (conv ctx)
-  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
+  let threadenter ctx = S.threadenter (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
@@ -1685,7 +1685,7 @@ struct
       List.iter handle_path (S.paths_as_set conv_ctx);
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
-  let threadenter ?(multiple=false) ctx = S.threadenter ~multiple (conv ctx)
+  let threadenter ctx = S.threadenter (conv ctx)
   let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 72890be4b4..3ec428014b 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -423,7 +423,7 @@ struct
         }
       in
       (* TODO: don't hd *)
-      List.hd (Spec.threadenter ctx None v [])
+      List.hd (Spec.threadenter ctx ~multiple:false None v [])
       (* TODO: do threadspawn to mainfuns? *)
     in
     let prestartstate = Spec.startstate MyCFG.dummy_func.svar in (* like in do_extern_inits *)
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index c88f3f00c1..73c160e3bb 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -179,7 +179,7 @@ struct
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
-  let threadenter ?(multiple=false) ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
+  let threadenter ctx  ~multiple lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
   let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
   let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
 end
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index 3c702d199f..45a547c471 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -76,7 +76,7 @@ struct
     step_ctx ctx
 
   let startstate v = `Lifted Automaton.initial
-  let threadenter ?(multiple=false) ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index ad32713fa8..1bf6294020 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -199,7 +199,7 @@ struct
     let r = Dom.bindings a in
     List.map (fun (x,v) -> (Dom.singleton x v, b)) r
 
-  let threadenter ?(multiple=false) ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let g xs x' ys =
       let ys' = List.map (fun y ->
           let yr = step ctx.prev_node (ctx.context ()) x' (ThreadEntry (lval, f, args)) (nosync x') in (* threadenter called on before-sync state *)

From 7ebddbc89f20e16927eafb6abafa3e79abde2fe8 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Sep 2023 13:48:47 +0200
Subject: [PATCH 04/19] Also pass to threadspawn for history TID + uniqueness

---
 src/analyses/abortUnless.ml                  |  2 +-
 src/analyses/accessAnalysis.ml               |  2 +-
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/expsplit.ml                     |  2 +-
 src/analyses/extractPthread.ml               |  2 +-
 src/analyses/fileUse.ml                      |  2 +-
 src/analyses/mCP.ml                          |  4 +-
 src/analyses/mallocFresh.ml                  |  2 +-
 src/analyses/malloc_null.ml                  |  2 +-
 src/analyses/mutexTypeAnalysis.ml            |  2 +-
 src/analyses/region.ml                       |  2 +-
 src/analyses/spec.ml                         |  2 +-
 src/analyses/symbLocks.ml                    |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/threadAnalysis.ml               |  2 +-
 src/analyses/threadEscape.ml                 |  2 +-
 src/analyses/threadFlag.ml                   |  2 +-
 src/analyses/threadId.ml                     |  8 +--
 src/analyses/threadJoins.ml                  |  2 +-
 src/analyses/tmpSpecial.ml                   |  2 +-
 src/analyses/tutorials/taint.ml              |  2 +-
 src/analyses/tutorials/unitAnalysis.ml       |  2 +-
 src/analyses/uninit.ml                       |  2 +-
 src/analyses/useAfterFree.ml                 |  2 +-
 src/analyses/varEq.ml                        |  2 +-
 src/cdomains/threadIdDomain.ml               | 55 ++++++++++----------
 src/framework/analyses.ml                    |  4 +-
 src/framework/constraints.ml                 | 30 +++++------
 src/util/wideningTokens.ml                   |  2 +-
 src/witness/observerAnalysis.ml              |  2 +-
 src/witness/witnessConstraints.ml            |  4 +-
 33 files changed, 80 insertions(+), 79 deletions(-)

diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index 5c24e61f7c..ee4db69820 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -66,7 +66,7 @@ struct
 
   let startstate v = false
   let threadenter ctx ~multiple lval f args = [false]
-  let threadspawn ctx lval f args fctx = false
+  let threadspawn ctx ~multiple lval f args fctx = false
   let exitstate v = false
 end
 
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index f0025c2f1c..b181a1c70e 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -121,7 +121,7 @@ struct
     ctx.local
 
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx  ~multiple lval f args fctx =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
     begin match lval with
       | None -> ()
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index c232ccae9b..13f549fc44 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -665,7 +665,7 @@ struct
       (* TODO: do something like base? *)
       failwith "relation.threadenter: unknown function"
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     ctx.local
 
   let event ctx e octx =
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index e824fac013..01646a54cf 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2513,7 +2513,7 @@ struct
       let st = special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) ctx.global st f args in
       [st]
 
-  let threadspawn ctx (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
+  let threadspawn ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
     begin match lval with
       | Some lval ->
         begin match ThreadId.get_current (Analyses.ask_of_ctx fctx) with
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 820ff69efa..3b23dc03fc 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -156,7 +156,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index 141a04283b..fef3d9ff9f 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -86,7 +86,7 @@ struct
 
   let threadenter ctx ~multiple lval f args = [ctx.local]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     emit_splits_ctx ctx
 
   let event ctx (event: Events.t) octx =
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index f72f72c1fe..f084a21edb 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1254,7 +1254,7 @@ module Spec : Analyses.MCPSpec = struct
     [ { f_d with pred = d.pred } ]
 
 
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 
   let exitstate v = D.top ()
 
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index b8e7fd78f5..58257b7843 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -288,7 +288,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 5259bdb6c7..7a7e787ad7 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -578,7 +578,7 @@ struct
     (* TODO: this do_emits is now different from everything else *)
     map (fun d -> do_emits ctx !emits d false) @@ map topo_sort_an @@ n_cartesian_product css
 
-  let threadspawn (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a fctx =
+  let threadspawn (ctx:(D.t, G.t, C.t, V.t) ctx) ~multiple lval f a fctx =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadspawn" ~sides ~emits ctx in
@@ -586,7 +586,7 @@ struct
     let f post_all (n,(module S:MCPSpec),(d,fd)) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadspawn" ~post_all ctx'' n d in
       let fctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadspawn" ~post_all fctx'' n fd in
-      n, repr @@ S.threadspawn ctx' lval f a fctx'
+      n, repr @@ S.threadspawn ~multiple ctx' lval f a fctx'
     in
     let d, q = map_deadcode f @@ spec_list2 ctx.local fctx.local in
     do_sideg ctx !sides;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index e171ad4ea1..b45573a801 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -55,7 +55,7 @@ struct
   let threadenter ctx ~multiple lval f args =
     [D.empty ()]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     D.empty ()
 
   module A =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 41c251dfce..f993db0c6e 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -216,7 +216,7 @@ struct
 
   let startstate v = D.empty ()
   let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
   let init marshal =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 66e60aede1..e640a261cd 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -66,7 +66,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 86cad5684b..652526543c 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -177,7 +177,7 @@ struct
 
   let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 
   let exitstate v = `Lifted (RegMap.bot ())
 
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index c44edd6c87..2f754f6160 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -488,7 +488,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 32be32f73d..f6fdd96c2e 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -30,7 +30,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let branch ctx exp tv = ctx.local
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index b45ea54877..88cf532ab2 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -103,7 +103,7 @@ struct
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args =
     [D.bot ()]
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     match lval with
     | Some lv -> taint_lval ctx lv
     | None -> ctx.local
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index ff4b4d5c63..f51e9395db 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -91,7 +91,7 @@ struct
        ctx.sideg tid (true, TS.bot (), false));
     [D.bot ()]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in
     let repeated = D.mem tid ctx.local in
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 0948a3976d..21a8b69c93 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -153,7 +153,7 @@ struct
   let threadenter ctx ~multiple lval f args =
     [D.bot ()]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     D.join ctx.local @@
     match args with
     | [ptc_arg] ->
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 81e05af679..6bd466caef 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -63,7 +63,7 @@ struct
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     D.join ctx.local (Flag.get_main ())
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index a9f3fa35f7..900870a676 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -58,8 +58,8 @@ struct
 
   let create_tid ?(multiple=false) (_, current, (td, _)) ((node, index): Node.t * int option) v =
     match current with
-    | `Lifted current when not multiple ->
-      let+ tid = Thread.threadenter (current, td) node index v in
+    | `Lifted current ->
+      let+ tid = Thread.threadenter ~multiple (current, td) node index v in
       if GobConfig.get_bool "dbg.print_tids" then
         Hashtbl.replace !tids tid ();
       `Lifted tid
@@ -138,10 +138,10 @@ struct
     let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let (current_n, current, (td,tdl)) = ctx.local in
     let v, n, i = match fctx.local with `Lifted vni, _, _ -> vni | _ -> failwith "ThreadId.threadspawn" in
-    (current_n, current, (Thread.threadspawn td n i v, Thread.threadspawn tdl n i v))
+    (current_n, current, (Thread.threadspawn ~multiple td n i v, Thread.threadspawn ~multiple tdl n i v))
 
   type marshal = (Thread.t,unit) Hashtbl.t (* TODO: don't use polymorphic Hashtbl *)
   let init (m:marshal option): unit =
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index f2cd36619f..862711073c 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -81,7 +81,7 @@ struct
       )
     | _, _ -> ctx.local
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     if D.is_bot ctx.local then ( (* bot is All threads *)
       M.info ~category:Imprecise "Thread created while ALL threads must-joined, continuing with no threads joined.";
       D.top () (* top is no threads *)
diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index 046345e627..9ed6da7c60 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -89,7 +89,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 7fc3fd7343..a978d0faf4 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -130,7 +130,7 @@ struct
   (* You may leave these alone *)
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 3ecddc2bc0..dc377cdd97 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -40,7 +40,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 2b388d1190..8693599a4d 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -26,7 +26,7 @@ struct
 
   let startstate v : D.t = D.empty ()
   let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
   let access_address (ask: Queries.ask) write lv =
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 0c7a46c35f..683ddbdcc2 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -197,7 +197,7 @@ struct
     | _ -> state
 
   let threadenter ctx ~multiple lval f args = [ctx.local]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 
   let startstate v = D.bot ()
   let exitstate v = D.top ()
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 3aaef95265..3f5a65516f 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -44,7 +44,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let typ_equal = CilType.Typ.equal (* TODO: Used to have equality checking, which ignores attributes. Is that needed? *)
diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
index 7193552048..a9646cffd2 100644
--- a/src/cdomains/threadIdDomain.ml
+++ b/src/cdomains/threadIdDomain.ml
@@ -23,7 +23,7 @@ module type Stateless =
 sig
   include S
 
-  val threadenter: Node.t -> int option -> varinfo -> t
+  val threadenter: multiple:bool -> Node.t -> int option -> varinfo -> t
 end
 
 module type Stateful =
@@ -32,8 +32,8 @@ sig
 
   module D: Lattice.S
 
-  val threadenter: t * D.t -> Node.t -> int option -> varinfo -> t list
-  val threadspawn: D.t -> Node.t -> int option -> varinfo -> D.t
+  val threadenter: multiple:bool -> t * D.t -> Node.t -> int option -> varinfo -> t list
+  val threadspawn: multiple:bool -> D.t -> Node.t -> int option -> varinfo -> D.t
 
   (** If it is possible to get a list of threads created thus far, get it *)
   val created: t -> D.t -> (t list) option
@@ -71,9 +71,10 @@ struct
 
   let threadinit v ~multiple: t = (v, None)
 
-  let threadenter l i v: t =
+  let threadenter ~multiple l i v: t =
     if GobConfig.get_bool "ana.thread.include-node" then
-      (v, Some (l, i))
+      let counter = Option.map (fun x -> if multiple then WrapperFunctionAnalysis0.ThreadCreateUniqueCount.top () else x) i in
+      (v, Some (l, counter))
     else
       (v, None)
 
@@ -93,8 +94,8 @@ struct
 
   module D = Lattice.Unit
 
-  let threadenter _ n i v = [threadenter n i v]
-  let threadspawn () _ _ _ = ()
+  let threadenter ~multiple _ n i v = [threadenter ~multiple n i v]
+  let threadspawn ~multiple () _ _ _ = ()
 
   let created _ _ = None
 end
@@ -162,10 +163,10 @@ struct
     else
       ([base_tid], S.empty ())
 
-  let threadenter ((p, _ ) as current, (cs,_)) (n: Node.t) i v =
-    let ni = Base.threadenter n i v in
+  let threadenter ~multiple ((p, _ ) as current, (cs,_)) (n: Node.t) i v =
+    let ni = Base.threadenter ~multiple n i v in
     let ((p', s') as composed) = compose current ni in
-    if is_unique composed && S.mem ni cs then
+    if is_unique composed && (S.mem ni cs || multiple) then
       [(p, S.singleton ni); composed] (* also respawn unique version of the thread to keep it reachable while thread ID sets refer to it *)
     else
       [composed]
@@ -182,12 +183,12 @@ struct
     in
     Some (List.concat_map map_one els)
 
-  let threadspawn (cs,cms) l i v =
-    let e = Base.threadenter l i v in
+  let threadspawn ~multiple (cs,cms) l i v =
+    let e = Base.threadenter ~multiple l i v in
     if S.mem e cs then
       (cs, S.add e cms)
     else
-      (S.add e cs, cms)
+      (S.add e cs, if multiple then S.add e cms else cms)
 
   let is_main = function
     | ([fl], s) when S.is_empty s && Base.is_main fl -> true
@@ -257,24 +258,24 @@ struct
     | (None, Some x'), `Top -> liftp x' (P.D.top ())
     | _ -> None
 
-  let threadenter x n i v =
+  let threadenter ~multiple x n i v =
     match x with
-    | ((Some x', None), `Lifted1 d) -> H.threadenter (x',d) n i v |> List.map (fun t -> (Some t, None))
-    | ((Some x', None), `Bot) -> H.threadenter (x',H.D.bot ()) n i v |> List.map (fun t -> (Some t, None))
-    | ((Some x', None), `Top) -> H.threadenter (x',H.D.top ()) n i v |> List.map (fun t -> (Some t, None))
-    | ((None, Some x'), `Lifted2 d) -> P.threadenter (x',d) n i v |> List.map (fun t -> (None, Some t))
-    | ((None, Some x'), `Bot) -> P.threadenter (x',P.D.bot ()) n i v |> List.map (fun t -> (None, Some t))
-    | ((None, Some x'), `Top) -> P.threadenter (x',P.D.top ()) n i v |> List.map (fun t -> (None, Some t))
+    | ((Some x', None), `Lifted1 d) -> H.threadenter ~multiple (x',d) n i v |> List.map (fun t -> (Some t, None))
+    | ((Some x', None), `Bot) -> H.threadenter ~multiple (x',H.D.bot ()) n i v |> List.map (fun t -> (Some t, None))
+    | ((Some x', None), `Top) -> H.threadenter ~multiple (x',H.D.top ()) n i v |> List.map (fun t -> (Some t, None))
+    | ((None, Some x'), `Lifted2 d) -> P.threadenter ~multiple (x',d) n i v |> List.map (fun t -> (None, Some t))
+    | ((None, Some x'), `Bot) -> P.threadenter ~multiple (x',P.D.bot ()) n i v |> List.map (fun t -> (None, Some t))
+    | ((None, Some x'), `Top) -> P.threadenter ~multiple (x',P.D.top ()) n i v |> List.map (fun t -> (None, Some t))
     | _ -> failwith "FlagConfiguredTID received a value where not exactly one component is set"
 
-  let threadspawn x n i v =
+  let threadspawn ~multiple x n i v =
     match x with
-    | `Lifted1 x' -> `Lifted1 (H.threadspawn x' n i v)
-    | `Lifted2 x' -> `Lifted2 (P.threadspawn x' n i v)
-    | `Bot when history_enabled () -> `Lifted1 (H.threadspawn (H.D.bot ()) n i v)
-    | `Bot  -> `Lifted2 (P.threadspawn (P.D.bot ()) n i v)
-    | `Top when history_enabled () -> `Lifted1 (H.threadspawn (H.D.top ()) n i v)
-    | `Top  -> `Lifted2 (P.threadspawn (P.D.top ()) n i v)
+    | `Lifted1 x' -> `Lifted1 (H.threadspawn ~multiple x' n i v)
+    | `Lifted2 x' -> `Lifted2 (P.threadspawn ~multiple x' n i v)
+    | `Bot when history_enabled () -> `Lifted1 (H.threadspawn  ~multiple (H.D.bot ()) n i v)
+    | `Bot  -> `Lifted2 (P.threadspawn  ~multiple (P.D.bot ()) n i v)
+    | `Top when history_enabled () -> `Lifted1 (H.threadspawn ~multiple (H.D.top ()) n i v)
+    | `Top  -> `Lifted2 (P.threadspawn ~multiple (P.D.top ()) n i v)
 
   let name () = "FlagConfiguredTID: " ^ if history_enabled () then H.name () else P.name ()
 end
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 3bb88a6ead..e1a4560003 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -447,7 +447,7 @@ sig
   val threadenter : (D.t, G.t, C.t, V.t) ctx -> multiple:bool -> lval option -> varinfo -> exp list -> D.t list
 
   (** Updates the local state of the creator thread using initial state of created thread. *)
-  val threadspawn : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
+  val threadspawn : (D.t, G.t, C.t, V.t) ctx -> multiple:bool -> lval option -> varinfo -> exp list -> (D.t, G.t, C.t, V.t) ctx -> D.t
 
   val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
 end
@@ -697,7 +697,7 @@ struct
     ctx.local
 
   let threadenter ctx ~multiple lval f args = [ctx.local]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
 end
 
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index ed492f4237..f474df6834 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -86,8 +86,8 @@ struct
   let threadenter ctx ~multiple lval f args =
     List.map D.lift @@ S.threadenter (conv ctx) ~multiple lval f args
 
-  let threadspawn ctx lval f args fctx =
-    D.lift @@ S.threadspawn (conv ctx) lval f args (conv fctx)
+  let threadspawn ctx ~multiple lval f args fctx =
+    D.lift @@ S.threadspawn (conv ctx) ~multiple lval f args (conv fctx)
 
   let paths_as_set ctx =
     List.map (fun x -> D.lift x) @@ S.paths_as_set (conv ctx)
@@ -170,8 +170,8 @@ struct
   let threadenter ctx ~multiple lval f args =
     S.threadenter (conv ctx) ~multiple lval f args
 
-  let threadspawn ctx lval f args fctx =
-    S.threadspawn (conv ctx) lval f args (conv fctx)
+  let threadspawn ctx ~multiple lval f args fctx =
+    S.threadspawn (conv ctx) ~multiple lval f args (conv fctx)
 
   let paths_as_set ctx = S.paths_as_set (conv ctx)
   let event ctx e octx = S.event (conv ctx) e (conv octx)
@@ -250,7 +250,7 @@ struct
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
   let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift_start_level) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
-  let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (lift ctx) (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let leq0 = function
     | `Top -> false
@@ -395,7 +395,7 @@ struct
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
 
   let threadenter ctx ~multiple lval f args = S.threadenter (conv ctx) ~multiple lval f args |> List.map (fun d -> (d, snd ctx.local))
-  let threadspawn ctx lval f args fctx = lift_fun ctx S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let enter ctx r f args =
     let m = snd ctx.local in
@@ -486,7 +486,7 @@ struct
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
   let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
-  let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx D.lift (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
 
   let event (ctx:(D.t,G.t,C.t,V.t) ctx) (e:Events.t) (octx:(D.t,G.t,C.t,V.t) ctx):D.t = lift_fun ctx D.lift S.event ((|>) (conv octx) % (|>) e) `Bot
 end
@@ -563,7 +563,7 @@ struct
     if !AnalysisState.postsolving then
       sideg (GVar.contexts f) (G.create_contexts (G.CSet.singleton c))
 
-  let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t) list ref =
+  let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
     let r = ref [] in
     let spawns = ref [] in
     (* now watch this ... *)
@@ -586,7 +586,7 @@ struct
       (* TODO: don't repeat for all paths that spawn same *)
       let ds = S.threadenter ~multiple ctx lval f args in
       List.iter (fun d ->
-          spawns := (lval, f, args, d) :: !spawns;
+          spawns := (lval, f, args, d, multiple) :: !spawns;
           match Cilfacade.find_varinfo_fundec f with
           | fd ->
             let c = S.context fd d in
@@ -618,14 +618,14 @@ struct
         }
       in
       (* TODO: don't forget path dependencies *)
-      let one_spawn (lval, f, args, fd) =
+      let one_spawn (lval, f, args, fd, multiple) =
         let rec fctx =
           { ctx with
             ask = (fun (type a) (q: a Queries.t) -> S.query fctx q)
           ; local = fd
           }
         in
-        S.threadspawn ctx' lval f args fctx
+        S.threadspawn ctx' ~multiple lval f args fctx
       in
       bigsqcup (List.map one_spawn spawns)
 
@@ -1266,9 +1266,9 @@ struct
     let g xs ys = (List.map (fun y -> D.singleton y) ys) @ xs in
     fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let fd1 = D.choose fctx.local in
-    map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))
+    map ctx (Spec.threadspawn ~multiple) (fun h -> h lval f args (conv fctx fd1))
 
   let sync ctx reason = map ctx Spec.sync (fun h -> h reason)
 
@@ -1450,7 +1450,7 @@ struct
   let combine_assign ctx = S.combine_assign (conv ctx)
   let special ctx = S.special (conv ctx)
   let threadenter ctx = S.threadenter (conv ctx)
-  let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
+  let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
   let asm ctx = S.asm (conv ctx)
@@ -1686,7 +1686,7 @@ struct
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
   let threadenter ctx = S.threadenter (conv ctx)
-  let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
+  let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
   let asm ctx = S.asm (conv ctx)
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 73c160e3bb..1816de90c7 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -180,6 +180,6 @@ struct
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
   let threadenter ctx  ~multiple lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
-  let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx lift' (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
   let event ctx e octx = lift_fun ctx lift' S.event ((|>) (conv octx) % (|>) e)
 end
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index 45a547c471..e8daf56155 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -77,7 +77,7 @@ struct
 
   let startstate v = `Lifted Automaton.initial
   let threadenter ctx ~multiple lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 1bf6294020..8dedf77a79 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -209,9 +209,9 @@ struct
       ys' @ xs
     in
     fold' ctx (Spec.threadenter ~multiple) (fun h -> h lval f args) g []
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     let fd1 = Dom.choose_key (fst fctx.local) in
-    map ctx Spec.threadspawn (fun h -> h lval f args (conv fctx fd1))
+    map ctx (Spec.threadspawn ~multiple) (fun h -> h lval f args (conv fctx fd1))
 
   let sync ctx reason =
     fold'' ctx Spec.sync (fun h -> h reason) (fun (a, async) x r a' ->

From 44ef0843efac4839f45f267f015ace6a27a88414 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Sep 2023 13:54:36 +0200
Subject: [PATCH 05/19] Add example for race despite uniqueness counter

---
 .../40-threadid/11-multiple-unique-counter.c     | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/regression/40-threadid/11-multiple-unique-counter.c

diff --git a/tests/regression/40-threadid/11-multiple-unique-counter.c b/tests/regression/40-threadid/11-multiple-unique-counter.c
new file mode 100644
index 0000000000..37c08ae61a
--- /dev/null
+++ b/tests/regression/40-threadid/11-multiple-unique-counter.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.thread.unique_thread_id_count 4
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+int main(void) {
+  // This should spawn a non-unique thread
+  unknown(t_fun);
+  return 0;
+}

From b718e46241c0c4f9b926620060a8743c3c49b6d7 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 28 Sep 2023 14:04:49 +0200
Subject: [PATCH 06/19] Add check that only one mainfun is specified to
 privatizations

---
 src/analyses/basePriv.ml   | 2 +-
 src/analyses/commonPriv.ml | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 0154924a1c..3843dda300 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -893,7 +893,7 @@ end
 module MinePrivBase =
 struct
   include NoFinalize
-  include ConfCheck.RequireMutexPathSensInit
+  include ConfCheck.RequireMutexPathSensOneMainInit
   include MutexGlobals (* explicit not needed here because G is Prod anyway? *)
 
   let thread_join ?(force=false) ask get e st = st
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 1b92cb320d..38a8dfe1b7 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -19,12 +19,14 @@ struct
       if not mutex_active then failwith "Privatization (to be useful) requires the 'mutex' analysis to be enabled (it is currently disabled)"
   end
 
-  module RequireMutexPathSensInit =
+  module RequireMutexPathSensOneMainInit =
   struct
     let init () =
       RequireMutexActivatedInit.init ();
       let mutex_path_sens = List.mem "mutex" (GobConfig.get_string_list "ana.path_sens") in
       if not mutex_path_sens then failwith "The activated privatization requires the 'mutex' analysis to be enabled & path sensitive (it is currently enabled, but not path sensitive)";
+      let mainfuns = List.length @@ GobConfig.get_list "mainfun" in
+      if not (mainfuns = 1) then failwith "The activated privatization requires exactly one main function to be specified";
       ()
   end
 

From 7ad12249c111c7dbdb906be7f57311c49a3a15be Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 16:52:50 +0200
Subject: [PATCH 07/19] Move GraphML witness options into witness.graphml
 (issue #1217)

---
 conf/ldv-races.json                           |  6 +-
 conf/svcomp-yaml.json                         |  4 +-
 conf/svcomp.json                              |  6 +-
 conf/svcomp21.json                            |  4 +-
 ...vcomp22-intervals-novareq-affeq-apron.json |  6 +-
 ...comp22-intervals-novareq-affeq-native.json |  6 +-
 ...omp22-intervals-novareq-octagon-apron.json |  6 +-
 ...p22-intervals-novareq-polyhedra-apron.json |  6 +-
 conf/svcomp22.json                            |  6 +-
 conf/svcomp23.json                            |  6 +-
 src/common/util/options.schema.json           | 93 ++++++++++---------
 src/framework/control.ml                      |  2 +-
 src/witness/myARG.ml                          |  4 +-
 src/witness/witness.ml                        | 14 +--
 sv-comp/sv-comp-run-no-overflow.py            |  2 +-
 sv-comp/sv-comp-run.py                        |  2 +-
 .../observer/path_nofun_true-unreach-call.c   |  2 +-
 17 files changed, 101 insertions(+), 74 deletions(-)

diff --git a/conf/ldv-races.json b/conf/ldv-races.json
index 01c60efc8d..2840bb368c 100644
--- a/conf/ldv-races.json
+++ b/conf/ldv-races.json
@@ -53,8 +53,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "solver": "td3",
   "sem": {
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
index e09d1c80d7..10a977ff47 100644
--- a/conf/svcomp-yaml.json
+++ b/conf/svcomp-yaml.json
@@ -76,7 +76,9 @@
     "region-offsets": true
   },
   "witness": {
-    "enabled": false,
+    "graphml": {
+      "enabled": false
+    },
     "yaml": {
       "enabled": true
     },
diff --git a/conf/svcomp.json b/conf/svcomp.json
index 913d43784b..87fef277c3 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -90,8 +90,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "pre": {
     "enabled": false
diff --git a/conf/svcomp21.json b/conf/svcomp21.json
index a19bfdb9d0..eda5cdfb88 100644
--- a/conf/svcomp21.json
+++ b/conf/svcomp21.json
@@ -64,6 +64,8 @@
     }
   },
   "witness": {
-    "id": "enumerate"
+    "graphml": {
+      "id": "enumerate"
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-affeq-apron.json b/conf/svcomp22-intervals-novareq-affeq-apron.json
index 7f72f5d0d8..1dafe0a76d 100644
--- a/conf/svcomp22-intervals-novareq-affeq-apron.json
+++ b/conf/svcomp22-intervals-novareq-affeq-apron.json
@@ -68,7 +68,9 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
\ No newline at end of file
diff --git a/conf/svcomp22-intervals-novareq-affeq-native.json b/conf/svcomp22-intervals-novareq-affeq-native.json
index 3ae1b19788..47b5cbbd8f 100644
--- a/conf/svcomp22-intervals-novareq-affeq-native.json
+++ b/conf/svcomp22-intervals-novareq-affeq-native.json
@@ -65,7 +65,9 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-octagon-apron.json b/conf/svcomp22-intervals-novareq-octagon-apron.json
index 3bf149800e..c6c7144cf6 100644
--- a/conf/svcomp22-intervals-novareq-octagon-apron.json
+++ b/conf/svcomp22-intervals-novareq-octagon-apron.json
@@ -68,7 +68,9 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22-intervals-novareq-polyhedra-apron.json b/conf/svcomp22-intervals-novareq-polyhedra-apron.json
index e4e513415a..e636b6fcdf 100644
--- a/conf/svcomp22-intervals-novareq-polyhedra-apron.json
+++ b/conf/svcomp22-intervals-novareq-polyhedra-apron.json
@@ -68,7 +68,9 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp22.json b/conf/svcomp22.json
index 85ea693375..09113a38c9 100644
--- a/conf/svcomp22.json
+++ b/conf/svcomp22.json
@@ -67,7 +67,9 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/conf/svcomp23.json b/conf/svcomp23.json
index 56474fbe2b..6f404060ba 100644
--- a/conf/svcomp23.json
+++ b/conf/svcomp23.json
@@ -90,7 +90,9 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 400dde06dc..5f2081e8d6 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -2279,24 +2279,56 @@
       "title": "witness",
       "type": "object",
       "properties": {
-        "enabled": {
-          "title": "witness.enabled",
-          "description": "Output witness",
-          "type": "boolean",
-          "default": true
-        },
-        "path": {
-          "title": "witness.path",
-          "description": "Witness output path",
-          "type": "string",
-          "default": "witness.graphml"
-        },
-        "id": {
-          "title": "witness.id",
-          "description": "Which witness node IDs to use? node/enumerate",
-          "type": "string",
-          "enum": ["node", "enumerate"],
-          "default": "node"
+        "graphml": {
+          "title": "witness.graphml",
+          "type": "object",
+          "properties": {
+            "enabled": {
+              "title": "witness.graphml.enabled",
+              "description": "Output GraphML witness",
+              "type": "boolean",
+              "default": true
+            },
+            "path": {
+              "title": "witness.graphml.path",
+              "description": "GraphML witness output path",
+              "type": "string",
+              "default": "witness.graphml"
+            },
+            "id": {
+              "title": "witness.graphml.id",
+              "description": "Which witness node IDs to use? node/enumerate",
+              "type": "string",
+              "enum": ["node", "enumerate"],
+              "default": "node"
+            },
+            "minimize": {
+              "title": "witness.graphml.minimize",
+              "description": "Try to minimize the witness",
+              "type": "boolean",
+              "default": false
+            },
+            "uncil": {
+              "title": "witness.graphml.uncil",
+              "description":
+                "Try to undo CIL control flow transformations in witness",
+              "type": "boolean",
+              "default": false
+            },
+            "stack": {
+              "title": "witness.graphml.stack",
+              "description": "Construct stacktrace-based witness nodes",
+              "type": "boolean",
+              "default": true
+            },
+            "unknown": {
+              "title": "witness.graphml.unknown",
+              "description": "Output witness for unknown result",
+              "type": "boolean",
+              "default": true
+            }
+          },
+          "additionalProperties": false
         },
         "invariant": {
           "title": "witness.invariant",
@@ -2376,31 +2408,6 @@
           },
           "additionalProperties": false
         },
-        "minimize": {
-          "title": "witness.minimize",
-          "description": "Try to minimize the witness",
-          "type": "boolean",
-          "default": false
-        },
-        "uncil": {
-          "title": "witness.uncil",
-          "description":
-            "Try to undo CIL control flow transformations in witness",
-          "type": "boolean",
-          "default": false
-        },
-        "stack": {
-          "title": "witness.stack",
-          "description": "Construct stacktrace-based witness nodes",
-          "type": "boolean",
-          "default": true
-        },
-        "unknown": {
-          "title": "witness.unknown",
-          "description": "Output witness for unknown result",
-          "type": "boolean",
-          "default": true
-        },
         "yaml": {
           "title": "witness.yaml",
           "type": "object",
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 9baa2dd1ca..fe43deb45f 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.enabled") || get_bool "exp.arg" in
+  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.graphml.enabled") || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index 62c705f5b1..068aed7a22 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -320,7 +320,7 @@ struct
 
 
   let rec next_opt' n = match n with
-    | Statement {sid; skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.uncil" -> (* TODO: use elocs instead? *)
+    | Statement {sid; skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.graphml.uncil" -> (* TODO: use elocs instead? *)
       let (e, if_true_next_n,  if_false_next_n) = partition_if_next (Arg.next n) in
       (* avoid infinite recursion with sid <> sid2 in if_nondet_var *)
       (* TODO: why physical comparison if_false_next_n != n doesn't work? *)
@@ -373,7 +373,7 @@ struct
       Question(e_cond, e_true, e_false, Cilfacade.typeOf e_false)
 
   let next_opt' n = match n with
-    | Statement {skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.uncil" -> (* TODO: use eloc instead? *)
+    | Statement {skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.graphml.uncil" -> (* TODO: use eloc instead? *)
       let (e_cond, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in
       if Node.location if_true_next_n = loc && Node.location if_false_next_n = loc then
         match Arg.next if_true_next_n, Arg.next if_false_next_n with
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 9f5a3c1801..2d94f4a18d 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -13,7 +13,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   let module Invariant = WitnessUtil.Invariant (Task) in
 
   let module TaskResult =
-    (val if get_bool "witness.stack" then
+    (val if get_bool "witness.graphml.stack" then
         (module StackTaskResult (Task.Cfg) (TaskResult) : WitnessTaskResult)
       else
         (module TaskResult)
@@ -24,7 +24,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   struct
     (* type node = N.t
     type edge = TaskResult.Arg.Edge.t *)
-    let minwitness = get_bool "witness.minimize"
+    let minwitness = get_bool "witness.graphml.minimize"
     let is_interesting_real from_node edge to_node =
       (* TODO: don't duplicate this logic with write_node, write_edge *)
       (* startlines aren't currently interesting because broken, see below *)
@@ -58,12 +58,12 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   let module N = Arg.Node in
   let module GML = XmlGraphMlWriter in
   let module GML =
-    (val match get_string "witness.id" with
+    (val match get_string "witness.graphml.id" with
       | "node" ->
         (module ArgNodeGraphMlWriter (N) (GML) : GraphMlWriter with type node = N.t)
       | "enumerate" ->
         (module EnumerateNodeGraphMlWriter (N) (GML))
-      | _ -> failwith "witness.id: illegal value"
+      | _ -> failwith "witness.graphml.id: illegal value"
     )
   in
   let module GML = DeDupGraphMlWriter (N) (GML) in
@@ -305,7 +305,7 @@ struct
 
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
-      (val if GobConfig.get_bool "witness.enabled" then (
+      (val if GobConfig.get_bool "witness.graphml.enabled" then (
            let module Arg = (val ArgTool.create entrystates) in
            let module Arg =
            struct
@@ -576,8 +576,8 @@ struct
 
     print_task_result (module TaskResult);
 
-    if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then (
-      let witness_path = get_string "witness.path" in
+    if get_bool "witness.graphml.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.graphml.unknown") then (
+      let witness_path = get_string "witness.graphml.path" in
       Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult)
     )
 
diff --git a/sv-comp/sv-comp-run-no-overflow.py b/sv-comp/sv-comp-run-no-overflow.py
index a3461b1a64..88ee2c0e53 100755
--- a/sv-comp/sv-comp-run-no-overflow.py
+++ b/sv-comp/sv-comp-run-no-overflow.py
@@ -13,7 +13,7 @@
 
 OVERVIEW = False # with True Goblint isn't executed
 # TODO: don't hard-code specification
-GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/no-overflow.prp --set witness.path {witness_filename} {code_filename} -v"
+GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/no-overflow.prp --set witness.graphml.path {witness_filename} {code_filename} -v"
 TIMEOUT = 10 # with some int that's Goblint timeout for single execution
 START = 1
 EXIT_ON_ERROR = True
diff --git a/sv-comp/sv-comp-run.py b/sv-comp/sv-comp-run.py
index af7cada051..977aa69ab6 100755
--- a/sv-comp/sv-comp-run.py
+++ b/sv-comp/sv-comp-run.py
@@ -13,7 +13,7 @@
 
 OVERVIEW = False # with True Goblint isn't executed
 # TODO: don't hard-code specification
-GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/unreach-call-__VERIFIER_error.prp --set witness.path {witness_filename} {code_filename}"
+GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/unreach-call-__VERIFIER_error.prp --set witness.graphml.path {witness_filename} {code_filename}"
 TIMEOUT = 30 # with some int that's Goblint timeout for single execution
 START = 1
 EXIT_ON_ERROR = True
diff --git a/tests/sv-comp/observer/path_nofun_true-unreach-call.c b/tests/sv-comp/observer/path_nofun_true-unreach-call.c
index 0cb70d23e9..cf1191e9fd 100644
--- a/tests/sv-comp/observer/path_nofun_true-unreach-call.c
+++ b/tests/sv-comp/observer/path_nofun_true-unreach-call.c
@@ -21,4 +21,4 @@ int main()
     return 0;
 }
 
-// ./goblint --enable ana.sv-comp --enable ana.wp --enable witness.uncil --disable ana.int.def_exc --enable ana.int.interval --set ana.activated '["base"]' --html tests/sv-comp/observer/path_nofun_true-unreach-call.c
+// ./goblint --enable ana.sv-comp --enable ana.wp --enable witness.graphml.uncil --disable ana.int.def_exc --enable ana.int.interval --set ana.activated '["base"]' --html tests/sv-comp/observer/path_nofun_true-unreach-call.c

From 8399258dc31e0f12bbeea04be749f730bac080e0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 17:01:12 +0200
Subject: [PATCH 08/19] Disable witness.graphml.enabled by default

---
 conf/ldv-races.json                                  | 1 +
 conf/svcomp.json                                     | 1 +
 conf/svcomp21.json                                   | 1 +
 conf/svcomp22-intervals-novareq-affeq-apron.json     | 1 +
 conf/svcomp22-intervals-novareq-affeq-native.json    | 1 +
 conf/svcomp22-intervals-novareq-octagon-apron.json   | 1 +
 conf/svcomp22-intervals-novareq-polyhedra-apron.json | 1 +
 conf/svcomp22.json                                   | 1 +
 conf/svcomp23.json                                   | 1 +
 src/common/util/options.schema.json                  | 2 +-
 10 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/conf/ldv-races.json b/conf/ldv-races.json
index 2840bb368c..8db800d74c 100644
--- a/conf/ldv-races.json
+++ b/conf/ldv-races.json
@@ -54,6 +54,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp.json b/conf/svcomp.json
index 87fef277c3..2c310c076d 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -91,6 +91,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp21.json b/conf/svcomp21.json
index eda5cdfb88..2e36e61d0c 100644
--- a/conf/svcomp21.json
+++ b/conf/svcomp21.json
@@ -65,6 +65,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate"
     }
   }
diff --git a/conf/svcomp22-intervals-novareq-affeq-apron.json b/conf/svcomp22-intervals-novareq-affeq-apron.json
index 1dafe0a76d..f7f7662b6a 100644
--- a/conf/svcomp22-intervals-novareq-affeq-apron.json
+++ b/conf/svcomp22-intervals-novareq-affeq-apron.json
@@ -69,6 +69,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp22-intervals-novareq-affeq-native.json b/conf/svcomp22-intervals-novareq-affeq-native.json
index 47b5cbbd8f..00db00f30f 100644
--- a/conf/svcomp22-intervals-novareq-affeq-native.json
+++ b/conf/svcomp22-intervals-novareq-affeq-native.json
@@ -66,6 +66,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp22-intervals-novareq-octagon-apron.json b/conf/svcomp22-intervals-novareq-octagon-apron.json
index c6c7144cf6..a0c09e8937 100644
--- a/conf/svcomp22-intervals-novareq-octagon-apron.json
+++ b/conf/svcomp22-intervals-novareq-octagon-apron.json
@@ -69,6 +69,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp22-intervals-novareq-polyhedra-apron.json b/conf/svcomp22-intervals-novareq-polyhedra-apron.json
index e636b6fcdf..3a478bf687 100644
--- a/conf/svcomp22-intervals-novareq-polyhedra-apron.json
+++ b/conf/svcomp22-intervals-novareq-polyhedra-apron.json
@@ -69,6 +69,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp22.json b/conf/svcomp22.json
index 09113a38c9..316c3c5534 100644
--- a/conf/svcomp22.json
+++ b/conf/svcomp22.json
@@ -68,6 +68,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/conf/svcomp23.json b/conf/svcomp23.json
index 6f404060ba..af584f1593 100644
--- a/conf/svcomp23.json
+++ b/conf/svcomp23.json
@@ -91,6 +91,7 @@
   },
   "witness": {
     "graphml": {
+      "enabled": true,
       "id": "enumerate",
       "unknown": false
     }
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 5f2081e8d6..8255be2b48 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -2287,7 +2287,7 @@
               "title": "witness.graphml.enabled",
               "description": "Output GraphML witness",
               "type": "boolean",
-              "default": true
+              "default": false
             },
             "path": {
               "title": "witness.graphml.path",

From 783442572bdc03837dd1378c71994e4f53bae360 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 17:27:09 +0200
Subject: [PATCH 09/19] Forbid witness.graphml.enabled outside of SV-COMP mode

---
 src/framework/control.ml | 2 +-
 src/maingoblint.ml       | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index fe43deb45f..948dce6075 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.graphml.enabled") || get_bool "exp.arg" in
+  let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index b5998df2d1..6c55f43ba1 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -160,7 +160,8 @@ let check_arguments () =
         ^ String.concat " and " @@ List.map (fun s -> "'" ^ s ^ "'") imprecise_options)
   );
   if get_bool "solvers.td3.space" && get_bool "solvers.td3.remove-wpoint" then fail "solvers.td3.space is incompatible with solvers.td3.remove-wpoint";
-  if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'"
+  if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'";
+  if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)"
 
 (** Initialize some globals in other modules. *)
 let handle_flags () =

From e01caccff051316ecb3ff26ba176656f06a9fb76 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 17:31:30 +0200
Subject: [PATCH 10/19] Disable witness.invariant.accessed by default

Makes access analysis more expensive
---
 src/common/util/options.schema.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 8255be2b48..188e5a77e8 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -2365,7 +2365,7 @@
               "title": "witness.invariant.accessed",
               "description": "Only emit invariants for locally accessed variables",
               "type": "boolean",
-              "default": true
+              "default": false
             },
             "full": {
               "title": "witness.invariant.full",

From 6cd62e5163aaaa5deb6ac046d6ab7995e358d1a1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 17:39:48 +0200
Subject: [PATCH 11/19] Update witness timings

---
 src/witness/witness.ml     | 7 ++-----
 src/witness/yamlWitness.ml | 3 +++
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 2d94f4a18d..af2e1c03ec 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -572,13 +572,13 @@ struct
 
   let write entrystates =
     let module Task = (val (BatOption.get !task)) in
-    let module TaskResult = (val (Timing.wrap "determine" (determine_result entrystates) (module Task))) in
+    let module TaskResult = (val (Timing.wrap "sv-comp result" (determine_result entrystates) (module Task))) in
 
     print_task_result (module TaskResult);
 
     if get_bool "witness.graphml.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.graphml.unknown") then (
       let witness_path = get_string "witness.graphml.path" in
-      Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult)
+      Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult)
     )
 
   let write entrystates =
@@ -595,7 +595,4 @@ struct
       )
       else
         write entrystates
-
-  let write entrystates =
-    Timing.wrap "witness" write entrystates
 end
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 72ff21f6bd..9e8ebeff51 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -392,6 +392,9 @@ struct
     ];
 
     yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
+
+  let write () =
+    Timing.wrap "yaml witness" write ()
 end
 
 

From 4d6b570d6d3c20850fcbe0e95f86638e8595c78b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 16:29:10 +0200
Subject: [PATCH 12/19] Add type for SV-COMP multiproperty

---
 src/autoTune.ml           | 21 ++++++++++++++-------
 src/util/loopUnrolling.ml |  7 ++++---
 src/witness/svcomp.ml     | 16 +++++++++-------
 src/witness/svcompSpec.ml |  9 +++++++++
 src/witness/witness.ml    | 10 +++++++---
 5 files changed, 43 insertions(+), 20 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index b96848c841..c00564bce7 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -210,8 +210,8 @@ let activateLongjmpAnalysesWhenRequired () =
     enableAnalyses longjmpAnalyses;
   )
 
-let focusOnMemSafetySpecification () =
-  match Svcomp.Specification.of_option () with
+let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
+  match spec with
   | ValidFree -> (* Enable the useAfterFree analysis *)
     let uafAna = ["useAfterFree"] in
     print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
@@ -244,8 +244,11 @@ let focusOnMemSafetySpecification () =
      enableAnalyses memSafetyAnas)
   | _ -> ()
 
-let focusOnSpecification () =
-  match Svcomp.Specification.of_option () with
+let focusOnMemSafetySpecification () =
+  List.iter focusOnMemSafetySpecification (Svcomp.Specification.of_option ())
+
+let focusOnSpecification (spec: Svcomp.Specification.t) =
+  match spec with
   | UnreachCall s -> ()
   | NoDataRace -> (*enable all thread analyses*)
     print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\"";
@@ -255,6 +258,9 @@ let focusOnSpecification () =
     set_bool "ana.int.interval" true
   | _ -> ()
 
+let focusOnSpecification () =
+  List.iter focusOnSpecification (Svcomp.Specification.of_option ())
+
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
 class enumVisitor = object
@@ -411,9 +417,10 @@ let congruenceOption factors file =
 let apronOctagonOption factors file =
   let locals =
     if List.mem "specification" (get_string_list "ana.autotune.activated" ) && get_string "ana.specification" <> "" then
-      match Svcomp.Specification.of_option () with
-      | NoOverflow -> 12
-      | _ -> 8
+      if List.mem Svcomp.Specification.NoOverflow (Svcomp.Specification.of_option ()) then
+        12
+      else
+        8
     else 8
   in let globals = 2 in
   let selectedLocals =
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 62d0f662f3..9a2f6c7b29 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -324,9 +324,10 @@ class loopUnrollingCallVisitor = object
           raise Found;
         | _ ->
           if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then (
-            match SvcompSpec.of_option () with
-            | UnreachCall s -> if info.vname = s then raise Found
-            | _ -> ()
+            List.iter (function
+                | SvcompSpec.UnreachCall s -> if info.vname = s then raise Found
+                | _ -> ()
+              ) (SvcompSpec.of_option ())
           );
           DoChildren
       )
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 22543d48a9..6d773f666b 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -8,7 +8,7 @@ module Specification = SvcompSpec
 module type Task =
 sig
   val file: Cil.file
-  val specification: Specification.t
+  val specification: Specification.multi
 
   module Cfg: MyCFG.CfgBidir
 end
@@ -18,9 +18,10 @@ let task: (module Task) option ref = ref None
 
 let is_error_function f =
   let module Task = (val (Option.get !task)) in
-  match Task.specification with
-  | UnreachCall f_spec -> f.vname = f_spec
-  | _ -> false
+  List.exists (function
+      | Specification.UnreachCall f_spec -> f.vname = f_spec
+      | _ -> false
+    ) Task.specification
 
 (* TODO: unused, but should be used? *)
 let is_special_function f =
@@ -30,9 +31,10 @@ let is_special_function f =
     | fname when String.starts_with fname "__VERIFIER" -> true
     | fname ->
       let module Task = (val (Option.get !task)) in
-      match Task.specification with
-      | UnreachCall f_spec -> fname = f_spec
-      | _ -> false
+      List.exists (function
+          | Specification.UnreachCall f_spec -> fname = f_spec
+          | _ -> false
+        ) Task.specification
   in
   is_svcomp && is_verifier
 
diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index 4a3da23d9b..185f1fbf67 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -12,6 +12,8 @@ type t =
   | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
   | ValidMemcleanup
 
+type multi = t list
+
 let of_string s =
   let s = String.strip s in
   let regexp_multiple = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
@@ -48,6 +50,8 @@ let of_string s =
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
+let of_string s: multi = [of_string s]
+
 let of_file path =
   let s = BatFile.with_file_in path BatIO.read_all in
   of_string s
@@ -77,3 +81,8 @@ let to_string spec =
     | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg
+
+let to_string spec =
+  match spec with
+  | [spec] -> to_string spec
+  | _ -> assert false (* TODO: aggregate *)
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 9f5a3c1801..310717b9c3 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -303,7 +303,7 @@ struct
     val find_invariant: Node.t -> Invariant.t
   end
 
-  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
+  let determine_result entrystates (module Task:Task) (spec: Svcomp.Specification.t): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
       (val if GobConfig.get_bool "witness.enabled" then (
            let module Arg = (val ArgTool.create entrystates) in
@@ -338,7 +338,7 @@ struct
       )
     in
 
-    match Task.specification with
+    match spec with
     | UnreachCall _ ->
       (* error function name is globally known through Svcomp.task *)
       let is_unreach_call =
@@ -410,7 +410,7 @@ struct
             let module TaskResult =
             struct
               module Arg = PathArg
-              let result = Result.False (Some Task.specification)
+              let result = Result.False (Some spec)
               let invariant _ = Invariant.none
               let is_violation = is_violation
               let is_sink _ = false
@@ -569,6 +569,10 @@ struct
         (module TaskResult:WitnessTaskResult)
       )
 
+  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
+    match Task.specification with
+    | [spec] -> determine_result entrystates (module Task) spec
+    | _ -> assert false (* TODO: aggregate *)
 
   let write entrystates =
     let module Task = (val (BatOption.get !task)) in

From 3747556e90acdced4e01fc21e9c83107d10f93fc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 17:23:40 +0200
Subject: [PATCH 13/19] Remove special MemorySafety SV-COMP property, add full
 multiproperty handling

---
 src/autoTune.ml           | 10 ----------
 src/witness/svcomp.ml     |  2 +-
 src/witness/svcompSpec.ml | 34 +++++++++++++++++-----------------
 src/witness/witness.ml    | 27 ++++++++++++++++++++++-----
 4 files changed, 40 insertions(+), 33 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index c00564bce7..06347f3190 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -232,16 +232,6 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
     );
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
-  | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
-    set_bool "ana.arrayoob" true;
-    (print_endline "Setting \"cil.addNestedScopeAttr\" to true";
-     set_bool "cil.addNestedScopeAttr" true;
-     if (get_int "ana.malloc.unique_address_count") < 1 then (
-       print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
-       set_int "ana.malloc.unique_address_count" 1;
-     );
-     let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
-     enableAnalyses memSafetyAnas)
   | _ -> ()
 
 let focusOnMemSafetySpecification () =
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 6d773f666b..736de0efae 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -45,6 +45,7 @@ struct
     | True
     | False of Specification.t option
     | Unknown
+  [@@deriving ord]
 
   let to_string = function
     | True -> "true"
@@ -57,7 +58,6 @@ struct
         | ValidFree -> "valid-free"
         | ValidDeref -> "valid-deref"
         | ValidMemtrack -> "valid-memtrack"
-        | MemorySafety -> "memory-safety" (* TODO: Currently here only to complete the pattern match *)
         | ValidMemcleanup -> "valid-memcleanup"
       in
       "false(" ^ result_spec ^ ")"
diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index 185f1fbf67..9bd5a35e3e 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -9,14 +9,13 @@ type t =
   | ValidFree
   | ValidDeref
   | ValidMemtrack
-  | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
   | ValidMemcleanup
+[@@deriving ord]
 
 type multi = t list
 
 let of_string s =
   let s = String.strip s in
-  let regexp_multiple = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_single = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
   if Str.string_match regexp_negated s 0 then
@@ -32,25 +31,29 @@ let of_string s =
         UnreachCall f
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
-  else if Str.string_match regexp_multiple s 0 then
-    let global1 = Str.matched_group 1 s in
-    let global2 = Str.matched_group 2 s in
-    let global3 = Str.matched_group 3 s in
-    let mem_safety_props = ["valid-free"; "valid-deref"; "valid-memtrack";] in
-    if (global1 <> global2 && global1 <> global3 && global2 <> global3) && List.for_all (fun x -> List.mem x mem_safety_props) [global1; global2; global3] then
-      MemorySafety
-    else
-      failwith "Svcomp.Specification.of_string: unknown global expression"
   else if Str.string_match regexp_single s 0 then
     let global = Str.matched_group 1 s in
-    if global = "valid-memcleanup" then
+    if global = "valid-free" then
+      ValidFree
+    else if global = "valid-deref" then
+      ValidDeref
+    else if global = "valid-memtrack" then
+      ValidMemtrack
+    else if global = "valid-memcleanup" then
       ValidMemcleanup
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
-let of_string s: multi = [of_string s]
+let of_string s: multi =
+  List.filter_map (fun line ->
+      let line = String.strip line in
+      if line = "" then
+        None
+      else
+        Some (of_string line)
+    ) (String.split_on_char '\n' s)
 
 let of_file path =
   let s = BatFile.with_file_in path BatIO.read_all in
@@ -77,12 +80,9 @@ let to_string spec =
     | ValidFree -> "valid-free", false
     | ValidDeref -> "valid-deref", false
     | ValidMemtrack -> "valid-memtrack", false
-    | MemorySafety -> "memory-safety", false (* TODO: That's false, it's currently here just to complete the pattern match *)
     | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg
 
 let to_string spec =
-  match spec with
-  | [spec] -> to_string spec
-  | _ -> assert false (* TODO: aggregate *)
+  String.concat "\n" (List.map to_string spec)
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 310717b9c3..419185400c 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -507,8 +507,7 @@ struct
       )
     | ValidFree
     | ValidDeref
-    | ValidMemtrack
-    | MemorySafety ->
+    | ValidMemtrack ->
       let module TrivialArg =
       struct
         include Arg
@@ -570,9 +569,27 @@ struct
       )
 
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
-    match Task.specification with
-    | [spec] -> determine_result entrystates (module Task) spec
-    | _ -> assert false (* TODO: aggregate *)
+    Task.specification
+    |> List.fold_left (fun acc spec ->
+        let module TaskResult = (val determine_result entrystates (module Task) spec) in
+        match acc with
+        | None -> Some (module TaskResult: WitnessTaskResult)
+        | Some (module Acc: WitnessTaskResult) ->
+          match Acc.result, TaskResult.result with
+          (* keep old violation/unknown *)
+          | False _, True
+          | False _, Unknown
+          | Unknown, True -> Some (module Acc: WitnessTaskResult)
+          (* use new violation/unknown *)
+          | True, False _
+          | Unknown, False _
+          | True, Unknown -> Some (module TaskResult: WitnessTaskResult)
+          (* both same, arbitrarily keep old *)
+          | True, True -> Some (module Acc: WitnessTaskResult)
+          | Unknown, Unknown -> Some (module Acc: WitnessTaskResult)
+          | False _, False _ -> failwith "multiple violations"
+      ) None
+    |> Option.get
 
   let write entrystates =
     let module Task = (val (BatOption.get !task)) in

From 5093b5dd90a6ec7aca4c541e007c7d4f3025b707 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 17:25:11 +0200
Subject: [PATCH 14/19] Fix witness determine_result for memsafety

---
 src/witness/witness.ml | 64 ++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 61 insertions(+), 3 deletions(-)

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 419185400c..dd829dd9e2 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -505,8 +505,66 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree
-    | ValidDeref
+    | ValidFree ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_free then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
+    | ValidDeref ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_deref then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
     | ValidMemtrack ->
       let module TrivialArg =
       struct
@@ -514,7 +572,7 @@ struct
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_free && not !AnalysisState.svcomp_may_invalid_deref && not !AnalysisState.svcomp_may_invalid_memtrack then (
+      if not !AnalysisState.svcomp_may_invalid_memtrack then (
         let module TaskResult =
         struct
           module Arg = Arg

From bb163a55ba1e06afcd267a02e521a4907f694db2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 19:13:04 +0200
Subject: [PATCH 15/19] Deduplicate Svcomp.is_error_function

---
 src/util/loopUnrolling.ml |  6 ++----
 src/witness/svcomp.ml     | 15 +++++++--------
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 9a2f6c7b29..4ce8fc06b4 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -324,10 +324,8 @@ class loopUnrollingCallVisitor = object
           raise Found;
         | _ ->
           if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then (
-            List.iter (function
-                | SvcompSpec.UnreachCall s -> if info.vname = s then raise Found
-                | _ -> ()
-              ) (SvcompSpec.of_option ())
+            if Svcomp.is_error_function' info (SvcompSpec.of_option ()) then
+              raise Found
           );
           DoChildren
       )
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 736de0efae..218f0716ae 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -16,12 +16,16 @@ end
 let task: (module Task) option ref = ref None
 
 
-let is_error_function f =
+let is_error_function' f spec =
   let module Task = (val (Option.get !task)) in
   List.exists (function
       | Specification.UnreachCall f_spec -> f.vname = f_spec
       | _ -> false
-    ) Task.specification
+    ) spec
+
+let is_error_function f =
+  let module Task = (val (Option.get !task)) in
+  is_error_function' f Task.specification
 
 (* TODO: unused, but should be used? *)
 let is_special_function f =
@@ -29,12 +33,7 @@ let is_special_function f =
   let is_svcomp = String.ends_with loc.file "sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
   let is_verifier = match f.vname with
     | fname when String.starts_with fname "__VERIFIER" -> true
-    | fname ->
-      let module Task = (val (Option.get !task)) in
-      List.exists (function
-          | Specification.UnreachCall f_spec -> fname = f_spec
-          | _ -> false
-        ) Task.specification
+    | fname -> is_error_function f
   in
   is_svcomp && is_verifier
 

From 031dde1e9538335a0691462a946b571866c1674b Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 1 Nov 2023 16:58:38 +0100
Subject: [PATCH 16/19] Add test for joinign thread array

---
 tests/regression/10-synch/28-join-array.c | 25 +++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 tests/regression/10-synch/28-join-array.c

diff --git a/tests/regression/10-synch/28-join-array.c b/tests/regression/10-synch/28-join-array.c
new file mode 100644
index 0000000000..99813b9810
--- /dev/null
+++ b/tests/regression/10-synch/28-join-array.c
@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] thread
+#include <pthread.h>
+
+int data = 0;
+pthread_mutex_t data_mutex;
+
+void *thread(void *arg) {
+  pthread_mutex_lock(&data_mutex);
+  data = 3; // RACE!
+  pthread_mutex_unlock(&data_mutex);
+  return NULL;
+}
+
+int main() {
+  pthread_t tids[2];
+
+  pthread_create(&tids[0], NULL, &thread, NULL);
+  pthread_create(&tids[1], NULL, &thread, NULL);
+
+  pthread_join(tids[0], NULL);
+
+  data = 1; //RACE!
+
+  return 1;
+}

From 1d55756147f3dba8cc5f42a996ae3ffaf7c6dbce Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 1 Nov 2023 16:59:08 +0100
Subject: [PATCH 17/19] threadAnalysis: Only add definite tids to set of
 mustJoined thread

---
 src/analyses/threadAnalysis.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 1e679a4707..1f6e9fabb3 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -61,7 +61,8 @@ struct
            s
        in
        match TS.elements (ctx.ask (Queries.EvalThread id)) with
-       | threads -> List.fold_left join_thread ctx.local threads
+       | [t] -> join_thread ctx.local t (* single thread *)
+       | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)
        | exception SetDomain.Unsupported _ -> ctx.local)
     | _ -> ctx.local
 

From f147d9bdd67fda7d77907631b643678eebe4284a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 2 Nov 2023 10:05:22 +0200
Subject: [PATCH 18/19] Remove unused [@@deriving ord] on SV-COMP spec

---
 src/witness/svcomp.ml     | 1 -
 src/witness/svcompSpec.ml | 1 -
 2 files changed, 2 deletions(-)

diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 218f0716ae..eae97b1199 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -44,7 +44,6 @@ struct
     | True
     | False of Specification.t option
     | Unknown
-  [@@deriving ord]
 
   let to_string = function
     | True -> "true"
diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index 9bd5a35e3e..66b3b83ac8 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -10,7 +10,6 @@ type t =
   | ValidDeref
   | ValidMemtrack
   | ValidMemcleanup
-[@@deriving ord]
 
 type multi = t list
 

From c42ec6b1e19eca1f1b899387a023d6505e285b7d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 26 Sep 2023 18:09:51 +0300
Subject: [PATCH 19/19] Refactor Access.may_race with match

---
 src/domains/access.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 8907ccbc32..3ba7aaee74 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -438,16 +438,13 @@ struct
 end
 
 
-(* Check if two accesses may race and if yes with which confidence *)
+(** Check if two accesses may race. *)
 let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} =
-  if kind = Read && kind2 = Read then
-    false (* two read/read accesses do not race *)
-  else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then
-    false
-  else if not (MCPAccess.A.may_race acc acc2) then
-    false (* analysis-specific information excludes race *)
-  else
-    true
+  match kind, kind2 with
+  | Read, Read -> false (* two read/read accesses do not race *)
+  | Free, _
+  | _, Free when not (get_bool "ana.race.free") -> false
+  | _, _ -> MCPAccess.A.may_race acc acc2 (* analysis-specific information excludes race *)
 
 (** Access sets for race detection and warnings. *)
 module WarnAccs =