From a50dc813320c2714b6bb0414e62a9897cc140370 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 3 Jun 2024 11:38:52 +0300
Subject: [PATCH 01/34] Unpin ppx_deriving

---
 dune-project          | 2 +-
 goblint.opam          | 4 +---
 goblint.opam.locked   | 8 ++------
 goblint.opam.template | 2 --
 gobview               | 2 +-
 5 files changed, 5 insertions(+), 13 deletions(-)

diff --git a/dune-project b/dune-project
index 878abd3b4f..c5adaddf81 100644
--- a/dune-project
+++ b/dune-project
@@ -29,7 +29,7 @@
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
-    ppx_deriving
+    (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
     (ounit2 :with-test)
diff --git a/goblint.opam b/goblint.opam
index 692625c965..0d8a561fa0 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -27,7 +27,7 @@ depends: [
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
-  "ppx_deriving"
+  "ppx_deriving" {>= "6.0.2"}
   "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
   "ounit2" {with-test}
@@ -79,8 +79,6 @@ available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
   [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
-  # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index f8de683948..d532457ced 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -81,10 +81,10 @@ depends: [
   "ounit2" {= "2.2.6" & with-test}
   "pp" {= "1.1.2"}
   "ppx_derivers" {= "1.2.1"}
-  "ppx_deriving" {= "5.2.1"}
+  "ppx_deriving" {= "6.0.2"}
   "ppx_deriving_hash" {= "0.1.2"}
   "ppx_deriving_yojson" {= "3.7.0"}
-  "ppxlib" {= "0.28.0"}
+  "ppxlib" {= "0.32.1"}
   "qcheck-core" {= "0.20"}
   "qcheck-ounit" {= "0.20" & with-test}
   "re" {= "1.10.4" & with-doc}
@@ -136,9 +136,5 @@ pin-depends: [
     "goblint-cil.2.0.3"
     "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
   ]
-  [
-    "ppx_deriving.5.2.1"
-    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
-  ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/goblint.opam.template b/goblint.opam.template
index 2d5ef10bc9..a730d5c064 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -4,8 +4,6 @@ available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
   [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
-  # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/gobview b/gobview
index 72abbb576b..195c61cbae 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 72abbb576b8ffc8759dcfa31501738f6b561b05a
+Subproject commit 195c61cbae86b8ffb8af4a21f2acd689665c1c0e

From 682eb0c183c897a31c8862c95a05bbc416437eb9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 4 Jun 2024 13:15:22 +0300
Subject: [PATCH 02/34] Refactor many privatizations to use
 LockDomain.MustLockset

---
 src/analyses/apron/relationPriv.apron.ml |   4 +-
 src/analyses/basePriv.ml                 | 102 +++++++++++------------
 src/analyses/commonPriv.ml               |  14 ++--
 src/cdomains/lockDomain.ml               |  16 ++++
 4 files changed, 75 insertions(+), 61 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 61da6ddc42..cada5ff888 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -579,7 +579,7 @@ struct
   let lock ask getg (st: relation_components_t) m =
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     (* TODO: somehow actually unneeded here? *)
-    if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if not atomic && Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
       let rel = st.rel in
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
@@ -1089,7 +1089,7 @@ struct
 
   let lock ask getg (st: relation_components_t) m =
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
-    if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if not atomic && Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
       let rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index cecc838b9e..f874232176 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -281,7 +281,7 @@ struct
      cpa' *)
 
   let lock ask getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
          where our (necessary) original context still has the mutex,
@@ -377,7 +377,7 @@ struct
      cpa' *)
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. *)
       let is_in_Gm x _ = is_protected_by ask m x in
@@ -523,7 +523,7 @@ struct
     {st with cpa = cpa'; priv = (W.add x w,LMust.add lm lmust,l')}
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
       let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
@@ -847,12 +847,12 @@ struct
 
   module GWeak =
   struct
-    include MapDomain.MapBot (Lockset) (WeakRange)
+    include MapDomain.MapBot (MustLockset) (WeakRange)
     let name () = "weak"
   end
   module GSync =
   struct
-    include MapDomain.MapBot (Lockset) (SyncRange)
+    include MapDomain.MapBot (MustLockset) (SyncRange)
     let name () = "synchronized"
   end
   module G =
@@ -908,10 +908,10 @@ struct
   let invariant_vars ask getg st =
     let module VS = Set.Make (CilType.Varinfo) in
     let s = current_lockset ask in
-    Lockset.fold (fun m acc ->
+    MustLockset.fold (fun m acc ->
         GSync.fold (fun s' cpa' acc ->
             SyncRange.fold_sync_vars VS.add cpa' acc
-          ) (G.sync (getg (V.mutex m))) acc
+          ) (G.sync (getg (V.mutex_mustlock m))) acc
       ) s VS.empty
     |> VS.elements
 end
@@ -987,7 +987,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
     GWeak.fold (fun s' tm acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           ThreadMap.fold (fun t' v acc ->
               VD.join v acc
             ) tm acc
@@ -1007,7 +1007,7 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
     let cpa' = GSync.fold (fun s' cpa' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           CPA.join cpa' acc
         else
           acc
@@ -1016,13 +1016,13 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove_addr m (current_lockset ask) in
     let t = current_thread ask in
     let side_cpa = CPA.filter (fun x _ ->
         GWeak.fold (fun s' tm acc ->
             (* TODO: swap 2^M and T partitioning for lookup by t here first? *)
             let v = ThreadMap.find t tm in
-            (Lockset.mem m s' && not (VD.is_bot v)) || acc
+            (MustLockset.mem_addr m s' && not (VD.is_bot v)) || acc
           ) (G.weak (getg (V.global x))) false
       ) st.cpa
     in
@@ -1048,7 +1048,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
     GWeak.fold (fun s' v acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           VD.join v acc
         else
           acc
@@ -1065,7 +1065,7 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
     let cpa' = GSync.fold (fun s' cpa' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           CPA.join cpa' acc
         else
           acc
@@ -1074,10 +1074,10 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove_addr m (current_lockset ask) in
     let side_cpa = CPA.filter (fun x _ ->
         GWeak.fold (fun s' v acc ->
-            (Lockset.mem m s' && not (VD.is_bot v)) || acc
+            (MustLockset.mem_addr m s' && not (VD.is_bot v)) || acc
           ) (G.weak (getg (V.global x))) false
       ) st.cpa
     in
@@ -1119,7 +1119,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
     GWeak.fold (fun s' v acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           VD.join v acc
         else
           acc
@@ -1140,7 +1140,7 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
     let cpa' = GSync.fold (fun s' cpa' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           CPA.join cpa' acc
         else
           acc
@@ -1149,7 +1149,7 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove_addr m (current_lockset ask) in
     let is_in_W x _ = W.mem x st.priv in
     let side_cpa = CPA.filter is_in_W st.cpa in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
@@ -1169,7 +1169,7 @@ struct
     if Param.side_effect_global_init then (
       CPA.fold (fun x v (st: BaseComponents (D).t) ->
           if is_global ask x then (
-            sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) v));
+            sideg (V.global x) (G.create_weak (GWeak.singleton (MustLockset.empty ()) v));
             {st with priv = W.add x st.priv} (* TODO: is this add necessary? *)
           )
           else
@@ -1222,7 +1222,7 @@ struct
 
   let startstate () = (DV.bot (), L.bot ())
 
-  let lockset_init = Lockset.top ()
+  let lockset_init = MustLockset.all ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
@@ -1241,7 +1241,7 @@ struct
           let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           MinLocksets.fold (fun b acc ->
               GSync.fold (fun s' cpa' acc ->
-                  if Lockset.disjoint b s' then
+                  if MustLockset.disjoint b s' then
                     let v = CPA.find x cpa' in
                     VD.join v acc
                   else
@@ -1254,7 +1254,7 @@ struct
     in
     let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_weak = GWeak.fold (fun s' v acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           VD.join v acc
         else
           acc
@@ -1301,7 +1301,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let sideg = Wrapper.sideg ask sideg in
     let getg = Wrapper.getg ask getg in
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove_addr m (current_lockset ask) in
     let is_in_G x _ = is_global ask x in
     let side_cpa = CPA.filter is_in_G st.cpa in
     let side_cpa = CPA.mapi (fun x v ->
@@ -1355,13 +1355,13 @@ struct
 
   module GWeakW =
   struct
-    include MapDomain.MapBot (Lockset) (VD)
+    include MapDomain.MapBot (MustLockset) (VD)
 
     let fold_weak f m a = fold (fun _ v a -> f v a) m a
   end
   module GSyncW =
   struct
-    include MapDomain.MapBot (Lockset) (LockCenteredBase.CPA)
+    include MapDomain.MapBot (MustLockset) (LockCenteredBase.CPA)
 
     let fold_sync_vars f m a =
       fold (fun _ cpa a ->
@@ -1393,11 +1393,11 @@ struct
 
   let startstate () = (W.bot (), P.top ())
 
-  let lockset_init = Lockset.top ()
+  let lockset_init = MustLockset.all ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
+      let v_init = GWeakW.find lockset_init (GWeak.find (MustLockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
       VD.join v v_init
     else
       v
@@ -1408,13 +1408,13 @@ struct
     let (w, p) = st.priv in
     let p_x = P.find x p in
     let d_cpa = CPA.find x st.cpa in
-    let d_sync = Lockset.fold (fun m acc ->
-        if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then
-          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
+    let d_sync = MustLockset.fold (fun m acc ->
+        if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then
+          let syncs = UnwrappedG.sync (getg (V.mutex_mustlock m)) in
           GSync.fold (fun s' gsyncw' acc ->
-              if Lockset.disjoint s s' then
+              if MustLockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
-                    if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+                    if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                       let v = CPA.find x cpa' in
                       VD.join v acc
                     else
@@ -1429,9 +1429,9 @@ struct
     in
     let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_weak = GWeak.fold (fun s' gweakw' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           GWeakW.fold (fun w' v acc ->
-              if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+              if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                 VD.join v acc
               else
                 acc
@@ -1471,7 +1471,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let getg = Wrapper.getg ask getg in
     let sideg = Wrapper.sideg ask sideg in
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove_addr m (current_lockset ask) in
     let (w, p) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
     if M.tracing then M.traceli "priv" "unlock %a %a" Lock.pretty m CPA.pretty st.cpa;
@@ -1507,7 +1507,7 @@ struct
         if EscapeDomain.EscapedVars.mem x escaped then (
           let (w, p) = st.priv in
           let p' = P.add x (MinLocksets.singleton s) p in
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa; priv = (w, p')}
         )
         else
@@ -1518,7 +1518,7 @@ struct
     let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
@@ -1548,11 +1548,11 @@ struct
 
   let startstate () = ((W.bot (), P.top ()), (DV.bot (), L.bot ()))
 
-  let lockset_init = Lockset.top ()
+  let lockset_init = MustLockset.all ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
+      let v_init = GWeakW.find lockset_init (GWeak.find (MustLockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
       VD.join v v_init
     else
       v
@@ -1568,9 +1568,9 @@ struct
           let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           MinLocksets.fold (fun b acc ->
               GSync.fold (fun s' gsyncw' acc ->
-                  if Lockset.disjoint b s' then
+                  if MustLockset.disjoint b s' then
                     GSyncW.fold (fun w' cpa' acc ->
-                        if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+                        if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                           let v = CPA.find x cpa' in
                           VD.join v acc
                         else
@@ -1586,9 +1586,9 @@ struct
     in
     let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_m_weak = GWeak.fold (fun s' gweakw' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           GWeakW.fold (fun w' v acc ->
-              if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+              if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                 VD.join v acc
               else
                 acc
@@ -1598,13 +1598,13 @@ struct
       ) weaks (VD.bot ())
     in
     let d_m = VD.join d_m_sync d_m_weak in
-    let d_g_sync = Lockset.fold (fun m acc ->
-        if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then
-          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
+    let d_g_sync = MustLockset.fold (fun m acc ->
+        if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then
+          let syncs = UnwrappedG.sync (getg (V.mutex_mustlock m)) in
           GSync.fold (fun s' gsyncw' acc ->
-              if Lockset.disjoint s s' then
+              if MustLockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
-                    if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+                    if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                       let v = CPA.find x cpa' in
                       VD.join v acc
                     else
@@ -1656,7 +1656,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let getg = Wrapper.getg ask getg in
     let sideg = Wrapper.sideg ask sideg in
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove_addr m (current_lockset ask) in
     let ((w, p), vl) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
     let side_gsyncw = CPA.fold (fun x v acc ->
@@ -1689,7 +1689,7 @@ struct
         if EscapeDomain.EscapedVars.mem x escaped then (
           let ((w, p), (vv, l)) = st.priv in
           let p' = P.add x (MinLocksets.singleton s) p in
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa; priv = ((w, p'), (vv, l))}
         )
         else
@@ -1700,7 +1700,7 @@ struct
     let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index aa829c4606..2334d76918 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -106,6 +106,7 @@ struct
     include Printable.Either3Conf (struct include Printable.DefaultConf let expand2 = false end) (VMutex) (VMutexInits) (VGlobal)
     let name () = "MutexGlobals"
     let mutex x: t = `Left x
+    let mutex_mustlock x = mutex (Addr (LockDomain.MustLock.to_mval x))
     let mutex_inits: t = `Middle ()
     let global x: t = `Right x
   end
@@ -136,17 +137,14 @@ struct
     let name () = "lock"
   end
 
-  module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
+  module MustLockset = LockDomain.MustLockset
 
-  module MustLockset = SetDomain.Reverse (Lockset)
-
-  let current_lockset (ask: Q.ask): Lockset.t =
+  let current_lockset (ask: Q.ask): MustLockset.t =
     (* TODO: remove this global_init workaround *)
     if !AnalysisState.global_initialization then
-      Lockset.empty ()
+      MustLockset.empty ()
     else
-      let mls = ask.f Queries.MustLockset in
-      LockDomain.MustLockset.fold (fun ml acc -> Lockset.add (Addr (LockDomain.MustLock.to_mval ml)) acc) mls (Lockset.empty ()) (* TODO: use MustLockset as Lockset *)
+      ask.f Queries.MustLockset
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
@@ -171,7 +169,7 @@ struct
     let name () = "P"
 
     (* TODO: change MinLocksets.exists/top instead? *)
-    let find x p = find_opt x p |? MinLocksets.singleton (Lockset.empty ()) (* ensure exists has something to check for thread returns *)
+    let find x p = find_opt x p |? MinLocksets.singleton (MustLockset.empty ()) (* ensure exists has something to check for thread returns *)
   end
 end
 
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 35d73e5f28..1c9fcb98c7 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -35,6 +35,22 @@ module MustLockset =
 struct
   include SetDomain.Reverse (SetDomain.ToppedSet (MustLock) (struct let topname = "All mutexes" end))
 
+  let mem_addr (a: Addr.t) (set: t) = (* TODO: replace with mem_mval *)
+    match Addr.to_mval a with
+    | Some mv when Mval.is_definite mv ->
+      let ml = MustLock.of_mval mv in
+      mem ml set
+    | _ ->
+      false
+
+  let remove_addr (a: Addr.t) (set: t) = (* TODO: replace with remove_mval *)
+    match Addr.to_mval a with
+    | Some mv when Mval.is_definite mv ->
+      let ml = MustLock.of_mval mv in
+      remove ml set
+    | _ ->
+      set
+
   let all (): t = `Top
   let is_all (set: t) = set = `Top
 end

From aeae2a97d2d475bba55ed2f0b8af94d497e7ab1c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 4 Jun 2024 16:37:20 +0300
Subject: [PATCH 03/34] Refactor privatizations' lock and unlock mutex type to
 Mustlock

---
 src/analyses/apron/relationPriv.apron.ml | 28 +++++++-------
 src/analyses/basePriv.ml                 | 48 ++++++++++++------------
 src/analyses/basePriv.mli                |  4 +-
 src/analyses/commonPriv.ml               | 18 ++++-----
 src/cdomains/lockDomain.ml               |  2 +
 5 files changed, 51 insertions(+), 49 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index cada5ff888..1302fa3743 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -33,8 +33,8 @@ module type S =
        the state when following conditional guards. *)
     val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> varinfo -> varinfo -> relation_components_t
 
-    val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
-    val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
+    val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
+    val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
 
     val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `Return | `Init | `Thread] -> relation_components_t
 
@@ -471,7 +471,7 @@ struct
 
   let startstate () = ()
 
-  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+  let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var
 
   let get_m_with_mutex_inits ask getg m =
     let get_m = getg (V.mutex m) in
@@ -577,9 +577,9 @@ struct
   let write_escape = write_global_internal ~skip_meet:true
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
     (* TODO: somehow actually unneeded here? *)
-    if not atomic && Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
+    if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
@@ -592,7 +592,7 @@ struct
       st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
     let rel = st.rel in
     if not atomic then (
       let rel_side = keep_only_protected_globals ask m rel in
@@ -703,7 +703,7 @@ module type ClusterArg = functor (RD: RelationDomain.RD) ->
 sig
   module LRD: Lattice.S
 
-  val keep_only_protected_globals: Q.ask -> LockDomain.Addr.t -> LRD.t -> LRD.t
+  val keep_only_protected_globals: Q.ask -> LockDomain.MustLock.t -> LRD.t -> LRD.t
   val keep_global: varinfo -> LRD.t -> LRD.t
 
   val lock: RD.t -> LRD.t -> LRD.t -> RD.t
@@ -962,7 +962,7 @@ struct
 
   let get_m_with_mutex_inits inits ask getg m =
     let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
-    if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.Addr.pretty m LRD.pretty get_m;
+    if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m;
     let r =
       if not inits then
         get_m
@@ -975,7 +975,7 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
     r
 
-  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+  let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
     let get_mutex_global_g =
@@ -1088,8 +1088,8 @@ struct
       {rel = rel_local; priv = (W.add g w,lmust,l)} (* Keep write local as if it were protected by the atomic section. *)
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
-    if not atomic && Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
+    if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
@@ -1112,7 +1112,7 @@ struct
     RD.keep_filter oct protected
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
     let rel = st.rel in
     let w,lmust,l = st.priv in
     if not atomic then (
@@ -1290,7 +1290,7 @@ struct
     r
 
   let lock ask getg st m =
-    if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
     let getg x =
       let r = getg x in
@@ -1302,7 +1302,7 @@ struct
     r
 
   let unlock ask getg sideg st m =
-    if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
     let getg x =
       let r = getg x in
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index f874232176..9dbffe40b1 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -28,8 +28,8 @@ sig
    * the state when following conditional guards. *)
   val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> varinfo -> VD.t -> BaseComponents (D).t
 
-  val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
-  val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
+  val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
+  val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
 
   val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseComponents (D).t
 
@@ -191,7 +191,7 @@ struct
     let get_mutex_inits = getg V.mutex_inits in
     let is_in_Gm x _ = is_protected_by ask m x in
     let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in
-    if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n  get_m: %a\n  get_mutex_inits: %a\n  get_mutex_inits': %a" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits';
+    if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n  get_m: %a\n  get_mutex_inits: %a\n  get_mutex_inits': %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits';
     CPA.join get_m get_mutex_inits'
 
   (** [get_m_with_mutex_inits] optimized for implementation-specialized [read_global]. *)
@@ -281,7 +281,7 @@ struct
      cpa' *)
 
   let lock ask getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
          where our (necessary) original context still has the mutex,
@@ -292,7 +292,7 @@ struct
          No other privatization uses is_unprotected, so this hack is only needed here. *)
       let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
       let cpa' = CPA.filter is_in_V get_m in
-      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.Addr.pretty m CPA.pretty cpa';
+      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pretty m CPA.pretty cpa';
       {st with cpa = CPA.fold CPA.add cpa' st.cpa}
     )
     else
@@ -301,7 +301,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     let side_m_cpa = CPA.filter is_in_Gm st.cpa in
-    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.Addr.pretty m CPA.pretty side_m_cpa;
+    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pretty m CPA.pretty side_m_cpa;
     sideg (V.mutex m) side_m_cpa;
     st
 
@@ -377,14 +377,14 @@ struct
      cpa' *)
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. *)
       let is_in_Gm x _ = is_protected_by ask m x in
       let get_m = CPA.filter is_in_Gm get_m in
       let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
       let meet = long_meet st.cpa get_m in
-      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet;
+      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet;
       {st with cpa = meet}
     )
     else
@@ -523,7 +523,7 @@ struct
     {st with cpa = cpa'; priv = (W.add x w,LMust.add lm lmust,l')}
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (MustLockset.mem_addr m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
       let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
@@ -750,7 +750,7 @@ struct
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let sideg = Wrapper.sideg ask sideg in
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
@@ -1016,13 +1016,13 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = MustLockset.remove_addr m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let t = current_thread ask in
     let side_cpa = CPA.filter (fun x _ ->
         GWeak.fold (fun s' tm acc ->
             (* TODO: swap 2^M and T partitioning for lookup by t here first? *)
             let v = ThreadMap.find t tm in
-            (MustLockset.mem_addr m s' && not (VD.is_bot v)) || acc
+            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
           ) (G.weak (getg (V.global x))) false
       ) st.cpa
     in
@@ -1074,10 +1074,10 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = MustLockset.remove_addr m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let side_cpa = CPA.filter (fun x _ ->
         GWeak.fold (fun s' v acc ->
-            (MustLockset.mem_addr m s' && not (VD.is_bot v)) || acc
+            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
           ) (G.weak (getg (V.global x))) false
       ) st.cpa
     in
@@ -1149,7 +1149,7 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = MustLockset.remove_addr m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let is_in_W x _ = W.mem x st.priv in
     let side_cpa = CPA.filter is_in_W st.cpa in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
@@ -1192,13 +1192,13 @@ struct
 
   module DV =
   struct
-    include MapDomain.MapBot_LiftTop (Lock) (MustVars)
+    include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MustVars)
     let name () = "V"
   end
 
   module L =
   struct
-    include MapDomain.MapBot_LiftTop (Lock) (MinLocksets)
+    include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MinLocksets)
     let name () = "L"
   end
 end
@@ -1301,7 +1301,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let sideg = Wrapper.sideg ask sideg in
     let getg = Wrapper.getg ask getg in
-    let s = MustLockset.remove_addr m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let is_in_G x _ = is_global ask x in
     let side_cpa = CPA.filter is_in_G st.cpa in
     let side_cpa = CPA.mapi (fun x v ->
@@ -1471,10 +1471,10 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let getg = Wrapper.getg ask getg in
     let sideg = Wrapper.sideg ask sideg in
-    let s = MustLockset.remove_addr m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let (w, p) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
-    if M.tracing then M.traceli "priv" "unlock %a %a" Lock.pretty m CPA.pretty st.cpa;
+    if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pretty m CPA.pretty st.cpa;
     let side_gsyncw = CPA.fold (fun x v acc ->
         if is_global ask x then (
           let w_x = W.find x w in
@@ -1487,7 +1487,7 @@ struct
           acc
       ) st.cpa (GSyncW.bot ())
     in
-    if M.tracing then M.traceu "priv" "unlock %a %a" Lock.pretty m GSyncW.pretty side_gsyncw;
+    if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pretty m GSyncW.pretty side_gsyncw;
     sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw));
     {st with priv = (w, p')}
 
@@ -1656,7 +1656,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let getg = Wrapper.getg ask getg in
     let sideg = Wrapper.sideg ask sideg in
-    let s = MustLockset.remove_addr m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let ((w, p), vl) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
     let side_gsyncw = CPA.fold (fun x v acc ->
@@ -1809,7 +1809,7 @@ struct
     r
 
   let lock ask getg st m =
-    if M.tracing then M.traceli "priv" "lock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
     let getg x =
       let r = getg x in
@@ -1821,7 +1821,7 @@ struct
     r
 
   let unlock ask getg sideg st m =
-    if M.tracing then M.traceli "priv" "unlock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
     let getg x =
       let r = getg x in
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
index e176a450fa..03a40405c0 100644
--- a/src/analyses/basePriv.mli
+++ b/src/analyses/basePriv.mli
@@ -17,8 +17,8 @@ sig
   val read_global: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> varinfo -> BaseDomain.VD.t
   val write_global: ?invariant:bool -> Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> varinfo -> BaseDomain.VD.t -> BaseDomain.BaseComponents (D).t
 
-  val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
-  val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
+  val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
+  val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
 
   val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
 
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index fe0611236c..5de56a8e59 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -74,12 +74,12 @@ struct
 
   let is_unprotected_without ask ?(write=true) ?(protection=Strong) x m: bool =
     (if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask) &&
-    ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=m; protection})
+    ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=Addr (LockDomain.MustLock.to_mval m); protection}) (* TODO: no mutex conversion? *)
 
   let is_protected_by ask ?(protection=Strong) m x: bool =
     is_global ask x &&
     not (VD.is_immediate_type x.vtype) &&
-    ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
+    ask.f (Q.MustBeProtectedBy {mutex=Addr (LockDomain.MustLock.to_mval m); global=x; write=true; protection}) (* TODO: no mutex conversion? *)
 
   let protected_vars (ask: Q.ask): varinfo list =
     LockDomain.MustLockset.fold (fun ml acc ->
@@ -92,7 +92,7 @@ module MutexGlobals =
 struct
   module VMutex =
   struct
-    include LockDomain.Addr
+    include LockDomain.MustLock
     let name () = "mutex"
   end
   module VMutexInits = Printable.UnitConf (struct let name = "MUTEX_INITS" end)
@@ -106,7 +106,7 @@ struct
     include Printable.Either3Conf (struct include Printable.DefaultConf let expand2 = false end) (VMutex) (VMutexInits) (VGlobal)
     let name () = "MutexGlobals"
     let mutex x: t = `Left x
-    let mutex_mustlock x = mutex (Addr (LockDomain.MustLock.to_mval x))
+    let mutex_mustlock x = mutex x (* TODO: remove *)
     let mutex_inits: t = `Middle ()
     let global x: t = `Right x
   end
@@ -250,7 +250,7 @@ struct
 
   module LLock =
   struct
-    include Printable.Either (Locksets.Lock) (struct include CilType.Varinfo let name () = "global" end)
+    include Printable.Either (LockDomain.MustLock) (struct include CilType.Varinfo let name () = "global" end)
     let mutex m = `Left m
     let global x = `Right x
   end
@@ -313,7 +313,7 @@ let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
   match addr with
   | UnknownPtr -> st
   | Addr (v, _) when ask.f (IsMultiple v) -> st
-  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st (LockDomain.MustLock.of_mval mv)
   | Addr _
   | NullPtr
   | StrPtr _ -> st
@@ -328,16 +328,16 @@ let lift_unlock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
   | UnknownPtr ->
     LockDomain.MustLockset.fold (fun ml st ->
         (* call privatization's unlock only with definite lock *)
-        f st (LockDomain.Addr.Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+        f st ml
       ) (ask.f MustLockset) st
   | StrPtr _
   | NullPtr -> st
-  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st (LockDomain.MustLock.of_mval mv)
   | Addr mv ->
     LockDomain.MustLockset.fold (fun ml st ->
         if LockDomain.MustLock.semantic_equal_mval ml mv = Some false then
           st
         else
           (* call privatization's unlock only with definite lock *)
-          f st (Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+          f st ml
       ) (ask.f MustLockset) st
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 1c9fcb98c7..be22ec1aea 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -24,6 +24,8 @@ struct
     else
       Some false
 
+  let of_var v: t = (v, `NoOffset)
+
   let of_mval ((v, o): Mval.t): t =
     (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o)
 

From 500b45236ecd10ccb85b60c87d3eecea40d30821 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 4 Jun 2024 16:38:33 +0300
Subject: [PATCH 04/34] Remove now-unnecessary must lockset functions

---
 src/analyses/basePriv.ml   |  6 +++---
 src/analyses/commonPriv.ml |  7 -------
 src/cdomains/lockDomain.ml | 16 ----------------
 3 files changed, 3 insertions(+), 26 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 9dbffe40b1..6deec0e8ca 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -911,7 +911,7 @@ struct
     MustLockset.fold (fun m acc ->
         GSync.fold (fun s' cpa' acc ->
             SyncRange.fold_sync_vars VS.add cpa' acc
-          ) (G.sync (getg (V.mutex_mustlock m))) acc
+          ) (G.sync (getg (V.mutex m))) acc
       ) s VS.empty
     |> VS.elements
 end
@@ -1410,7 +1410,7 @@ struct
     let d_cpa = CPA.find x st.cpa in
     let d_sync = MustLockset.fold (fun m acc ->
         if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then
-          let syncs = UnwrappedG.sync (getg (V.mutex_mustlock m)) in
+          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           GSync.fold (fun s' gsyncw' acc ->
               if MustLockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
@@ -1600,7 +1600,7 @@ struct
     let d_m = VD.join d_m_sync d_m_weak in
     let d_g_sync = MustLockset.fold (fun m acc ->
         if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then
-          let syncs = UnwrappedG.sync (getg (V.mutex_mustlock m)) in
+          let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           GSync.fold (fun s' gsyncw' acc ->
               if MustLockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 5de56a8e59..257fe9a038 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -106,7 +106,6 @@ struct
     include Printable.Either3Conf (struct include Printable.DefaultConf let expand2 = false end) (VMutex) (VMutexInits) (VGlobal)
     let name () = "MutexGlobals"
     let mutex x: t = `Left x
-    let mutex_mustlock x = mutex x (* TODO: remove *)
     let mutex_inits: t = `Middle ()
     let global x: t = `Right x
   end
@@ -131,12 +130,6 @@ end
 
 module Locksets =
 struct
-  module Lock =
-  struct
-    include LockDomain.Addr
-    let name () = "lock"
-  end
-
   module MustLockset = LockDomain.MustLockset
 
   let current_lockset (ask: Q.ask): MustLockset.t =
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index be22ec1aea..08353f4795 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -37,22 +37,6 @@ module MustLockset =
 struct
   include SetDomain.Reverse (SetDomain.ToppedSet (MustLock) (struct let topname = "All mutexes" end))
 
-  let mem_addr (a: Addr.t) (set: t) = (* TODO: replace with mem_mval *)
-    match Addr.to_mval a with
-    | Some mv when Mval.is_definite mv ->
-      let ml = MustLock.of_mval mv in
-      mem ml set
-    | _ ->
-      false
-
-  let remove_addr (a: Addr.t) (set: t) = (* TODO: replace with remove_mval *)
-    match Addr.to_mval a with
-    | Some mv when Mval.is_definite mv ->
-      let ml = MustLock.of_mval mv in
-      remove ml set
-    | _ ->
-      set
-
   let all (): t = `Top
   let is_all (set: t) = set = `Top
 end

From 90fc5aa1af4b0b734289917c3f713b5bf326a408 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 4 Jun 2024 16:51:16 +0300
Subject: [PATCH 05/34] Refine MustBeProtectedBy and MayBePublicWithout query
 mutex type

---
 src/analyses/commonPriv.ml    | 4 ++--
 src/analyses/mutexAnalysis.ml | 5 ++---
 src/domains/queries.ml        | 4 ++--
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 257fe9a038..3673991fda 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -74,12 +74,12 @@ struct
 
   let is_unprotected_without ask ?(write=true) ?(protection=Strong) x m: bool =
     (if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask) &&
-    ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=Addr (LockDomain.MustLock.to_mval m); protection}) (* TODO: no mutex conversion? *)
+    ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=m; protection})
 
   let is_protected_by ask ?(protection=Strong) m x: bool =
     is_global ask x &&
     not (VD.is_immediate_type x.vtype) &&
-    ask.f (Q.MustBeProtectedBy {mutex=Addr (LockDomain.MustLock.to_mval m); global=x; write=true; protection}) (* TODO: no mutex conversion? *)
+    ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
 
   let protected_vars (ask: Q.ask): varinfo list =
     LockDomain.MustLockset.fold (fun ml acc ->
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index b44795b6da..9b6aa4f4ca 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -209,15 +209,14 @@ struct
       MustLockset.disjoint held_locks protecting
     | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false
     | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} ->
-      let held_locks = MustLocksetRW.to_must_lockset @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in
+      let held_locks = MustLockset.remove without_mutex (MustLocksetRW.to_must_lockset ls) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then
         false
       else *)
       MustLockset.disjoint held_locks protecting
-    | Queries.MustBeProtectedBy {mutex = Addr mutex_mv; global=v; write; protection} when Mval.is_definite mutex_mv -> (* only definite Addrs can be in must-locksets to begin with, anything else cannot protect anything *)
-      let ml = LockDomain.MustLock.of_mval mutex_mv in
+    | Queries.MustBeProtectedBy {mutex = ml; global=v; write; protection} ->
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index a904f696eb..edb5c44c56 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -49,8 +49,8 @@ end
 
 (* Helper definitions for deriving complex parts of Any.compare below. *)
 type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
-type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t; protection: Protection.t} [@@deriving ord, hash]
-type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
+type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash]
+type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
 type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash]
 type access =
   | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *)

From b9badb75d61cc013352afdb39e3bd29aad3ff53f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Sat, 8 Jun 2024 11:19:22 +0300
Subject: [PATCH 06/34] Bump and pin apron to v0.9.15

For breaking change: https://github.com/antoinemine/apron/pull/108.
---
 dune-project          | 2 +-
 goblint.opam          | 6 +++++-
 goblint.opam.locked   | 6 +++++-
 goblint.opam.template | 1 +
 4 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/dune-project b/dune-project
index 878abd3b4f..751876f6b0 100644
--- a/dune-project
+++ b/dune-project
@@ -54,7 +54,7 @@
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
   )
   (depopts
-    apron
+    (apron (>= v0.9.15))
     z3
   )
   (conflicts
diff --git a/goblint.opam b/goblint.opam
index 692625c965..ec6a1f8fcb 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -51,7 +51,10 @@ depends: [
   "benchmark" {with-test}
   "conf-gcc"
 ]
-depopts: ["apron" "z3"]
+depopts: [
+  "apron" {>= "v0.9.15"}
+  "z3"
+]
 conflicts: [
   "result" {< "1.5"}
   "ez-conf-lib" {= "1"}
@@ -81,6 +84,7 @@ pin-depends: [
   [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#b3172bd51e4bb0135716a300cab424a56970d96f" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index f8de683948..8b184e189d 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -22,7 +22,7 @@ doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.14~beta.2"}
+  "apron" {= "v0.9.15"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
@@ -140,5 +140,9 @@ pin-depends: [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
   ]
+  [
+    "apron.v0.9.15"
+    "git+https://github.com/antoinemine/apron.git#b3172bd51e4bb0135716a300cab424a56970d96f"
+  ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/goblint.opam.template b/goblint.opam.template
index 2d5ef10bc9..27be21015f 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -6,6 +6,7 @@ pin-depends: [
   [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#b3172bd51e4bb0135716a300cab424a56970d96f" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

From ec675d4afc599d86b00e3b25b4f04946215f225f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Sat, 8 Jun 2024 11:26:27 +0300
Subject: [PATCH 07/34] Use Apron.Environment.cmp

---
 src/cdomains/apron/affineEqualityDomain.apron.ml       | 4 ++--
 src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 7e60cce74b..75c12a0e63 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -257,7 +257,7 @@ struct
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
 
   let leq t1 t2 =
-    let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
+    let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *)
     if env_comp = -2 || env_comp > 0 then
       (* -2:  environments are not compatible (a variable has different types in the 2 environements *)
       (* -1: if env1 is a subset of env2,  (OK)  *)
@@ -334,7 +334,7 @@ struct
     else
       match Option.get a.d, Option.get b.d with
       | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env}
-      | x, y when (Environment.compare a.env b.env <> 0) ->
+      | x, y when (Environment.cmp a.env b.env <> 0) ->
         let sup_env = Environment.lce a.env b.env in
         let mod_x = dim_add (Environment.dimchange a.env sup_env) x in
         let mod_y = dim_add (Environment.dimchange b.env sup_env) y in
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index 67bd67f4e5..b5f3bb5304 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -386,7 +386,7 @@ struct
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
 
   let leq t1 t2 =
-    let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
+    let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *)
     let implies ts i (var, b) =
       let tuple_cmp = Tuple2.eq (Option.eq ~eq:Int.equal) (Z.equal) in
       match var with
@@ -450,7 +450,7 @@ struct
     | Some x, Some y when is_top a || is_top b ->
       let new_env = Environment.lce a.env b.env in
       top_of new_env
-    | Some x, Some y when (Environment.compare a.env b.env <> 0) ->
+    | Some x, Some y when (Environment.cmp a.env b.env <> 0) ->
       let sup_env = Environment.lce a.env b.env in
       let mod_x = dim_add (Environment.dimchange a.env sup_env) x in
       let mod_y = dim_add (Environment.dimchange b.env sup_env) y in

From 794b6ec21cc24bbd790518ede62bb85bbce5b98e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Sat, 8 Jun 2024 11:28:50 +0300
Subject: [PATCH 08/34] Implement GobApron.Environment.compare with TODO

---
 src/cdomains/apron/gobApron.apron.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index c39a3e42db..40867f4889 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -42,6 +42,10 @@ module Environment =
 struct
   include Environment
 
+  let compare (x: t) (y: t): int =
+    (* TODO: implement total Environment order in OCaml *)
+    failwith "Apron.Environment doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
+
   let ivars_only env =
     let ivs, fvs = Environment.vars env in
     assert (Array.length fvs = 0); (* shouldn't ever contain floats *)

From a371b96d6c08177ff90545fc490ca40c69917077 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Sat, 8 Jun 2024 11:35:02 +0300
Subject: [PATCH 09/34] Remove broken Apron.Abstract1.compare

---
 src/cdomains/apron/apronDomain.apron.ml | 6 +++---
 src/cdomains/apron/gobApron.apron.ml    | 4 +++-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d0ef268ca6..9bf17b2f92 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -451,9 +451,9 @@ struct
   let hash (x:t) =
     A.hash Man.mgr x
 
-  let compare (x:t) y: int =
-    (* there is no A.compare, but polymorphic compare should delegate to Abstract0 and Environment compare's implemented in Apron's C *)
-    Stdlib.compare x y
+  let compare (x: t) (y: t): int =
+    failwith "Apron.Abstract1 doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
+
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)))
 
   let to_yojson (x: t) =
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index 40867f4889..46a0bbc28d 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -12,7 +12,9 @@ struct
   include Lincons1
 
   let show = Format.asprintf "%a" print
-  let compare x y = String.compare (show x) (show y) (* HACK *)
+  let compare x y =
+    (* TODO: implement proper total Lincons1 order *)
+    String.compare (show x) (show y) (* HACK *)
 
   let num_vars x =
     (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)

From a74840942fabc3231eb41eb62ce073a35b667971 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 21 Jun 2024 13:20:34 +0300
Subject: [PATCH 10/34] Upgrade locked opam dependencies

---
 goblint.opam.locked | 91 ++++++++++++++++++++++++---------------------
 gobview             |  2 +-
 2 files changed, 49 insertions(+), 44 deletions(-)

diff --git a/goblint.opam.locked b/goblint.opam.locked
index d532457ced..410d363ac8 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -21,89 +21,94 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
-  "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.14~beta.2"}
+  "angstrom" {= "0.16.0"}
+  "apron" {= "v0.9.14"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
   "base-bytes" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
-  "batteries" {= "3.6.0"}
+  "batteries" {= "3.8.0"}
   "benchmark" {= "1.6" & with-test}
   "bigarray-compat" {= "1.1.0"}
-  "bigstringaf" {= "0.9.0"}
+  "bigstringaf" {= "0.9.1"}
   "bos" {= "0.2.1"}
-  "camlidl" {= "1.11"}
+  "camlidl" {= "1.12"}
   "camlp-streams" {= "5.0.1"}
   "catapult" {= "0.2"}
   "catapult-file" {= "0.2"}
-  "cmdliner" {= "1.1.1" & with-doc}
-  "conf-autoconf" {= "0.1"}
+  "cmdliner" {= "1.3.0" & with-doc}
+  "conf-autoconf" {= "0.2"}
+  "conf-findutils" {= "1"}
   "conf-gcc" {= "1.0"}
   "conf-gmp" {= "4"}
-  "conf-mpfr" {= "3"}
+  "conf-gmp-paths" {= "1"}
+  "conf-mpfr-paths" {= "1"}
   "conf-perl" {= "2"}
-  "conf-pkg-config" {= "2"}
   "conf-ruby" {= "1.0.0" & with-test}
-  "conf-which" {= "1"}
   "cppo" {= "1.6.9"}
   "cpu" {= "2.0.0"}
-  "csexp" {= "1.5.1"}
-  "ctypes" {= "0.20.1"}
-  "dune" {= "3.7.1"}
-  "dune-build-info" {= "3.7.1"}
-  "dune-configurator" {= "3.7.1"}
-  "dune-private-libs" {= "3.7.1"}
-  "dune-site" {= "3.7.1"}
-  "dyn" {= "3.7.1"}
+  "crunch" {= "3.3.1" & with-doc}
+  "csexp" {= "1.5.2"}
+  "cstruct" {= "6.2.0"}
+  "ctypes" {= "0.22.0"}
+  "dune" {= "3.16.0"}
+  "dune-build-info" {= "3.16.0"}
+  "dune-configurator" {= "3.16.0"}
+  "dune-private-libs" {= "3.16.0"}
+  "dune-site" {= "3.16.0"}
+  "dyn" {= "3.16.0"}
+  "ez-conf-lib" {= "2"}
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
   "goblint-cil" {= "2.0.3"}
+  "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
-  "json-data-encoding" {= "0.12.1"}
-  "jsonrpc" {= "1.15.0~5.0preview1"}
+  "json-data-encoding" {= "1.0.1"}
+  "jsonrpc" {= "1.17.0"}
   "logs" {= "0.7.0"}
-  "mlgmpidl" {= "1.2.15"}
-  "num" {= "1.4"}
+  "mlgmpidl" {= "1.3.0"}
+  "num" {= "1.5"}
   "ocaml" {= "4.14.0"}
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocaml-config" {= "2"}
   "ocaml-option-flambda" {= "1"}
   "ocaml-syntax-shims" {= "1.0.0"}
   "ocaml-variants" {= "4.14.0+options"}
-  "ocamlbuild" {= "0.14.2"}
-  "ocamlfind" {= "1.9.5"}
-  "odoc" {= "2.2.0" & with-doc}
-  "odoc-parser" {= "2.0.0" & with-doc}
-  "ordering" {= "3.7.1"}
-  "ounit2" {= "2.2.6" & with-test}
-  "pp" {= "1.1.2"}
+  "ocamlbuild" {= "0.14.3"}
+  "ocamlfind" {= "1.9.6"}
+  "odoc" {= "2.4.2" & with-doc}
+  "odoc-parser" {= "2.4.2" & with-doc}
+  "ordering" {= "3.16.0"}
+  "ounit2" {= "2.2.7" & with-test}
+  "pp" {= "1.2.0"}
   "ppx_derivers" {= "1.2.1"}
   "ppx_deriving" {= "6.0.2"}
   "ppx_deriving_hash" {= "0.1.2"}
-  "ppx_deriving_yojson" {= "3.7.0"}
+  "ppx_deriving_yojson" {= "3.8.0"}
   "ppxlib" {= "0.32.1"}
-  "qcheck-core" {= "0.20"}
-  "qcheck-ounit" {= "0.20" & with-test}
-  "re" {= "1.10.4" & with-doc}
-  "result" {= "1.5"}
+  "ptime" {= "1.1.0" & with-doc}
+  "qcheck-core" {= "0.21.3"}
+  "qcheck-ounit" {= "0.21.3" & with-test}
+  "re" {= "1.11.0" & with-doc}
+  "result" {= "1.5" & with-doc}
   "rresult" {= "0.7.0"}
   "seq" {= "base"}
-  "sexplib0" {= "v0.15.1"}
-  "sha" {= "1.15.2"}
+  "sexplib0" {= "v0.16.0"}
+  "sha" {= "1.15.4"}
   "stdlib-shims" {= "0.3.0"}
-  "stdune" {= "3.7.1"}
+  "stdune" {= "3.16.0"}
   "stringext" {= "1.6.0"}
-  "topkg" {= "1.0.6"}
-  "tyxml" {= "4.5.0" & with-doc}
-  "uri" {= "4.2.0"}
+  "topkg" {= "1.0.7"}
+  "tyxml" {= "4.6.0" & with-doc}
+  "uri" {= "4.4.0"}
   "uuidm" {= "0.9.8"}
   "uutf" {= "1.0.3" & with-doc}
-  "yaml" {= "3.1.0"}
-  "yojson" {= "2.0.2"}
-  "zarith" {= "1.12"}
+  "yaml" {= "3.2.0"}
+  "yojson" {= "2.2.1"}
+  "zarith" {= "1.13"}
 ]
 build: [
   ["dune" "subst"] {dev}
diff --git a/gobview b/gobview
index 195c61cbae..287bf59be9 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 195c61cbae86b8ffb8af4a21f2acd689665c1c0e
+Subproject commit 287bf59be9e25ceea704384c65e0d91565bb749d

From a1bfc416569028f2f03c43d5df9840e2ac9aa3e6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 26 Jun 2024 11:45:25 +0300
Subject: [PATCH 11/34] Upgrade locked OCaml to 4.14.2

---
 .github/workflows/coverage.yml | 2 +-
 .github/workflows/docs.yml     | 2 +-
 .github/workflows/locked.yml   | 6 +++---
 .github/workflows/unlocked.yml | 8 ++++----
 goblint.opam.locked            | 4 ++--
 gobview                        | 2 +-
 make.sh                        | 2 +-
 7 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index d4fc872620..1e1991e2ab 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 242acef3de..bae49437dd 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 18935725ca..a7f8787305 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -20,7 +20,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -73,7 +73,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -116,7 +116,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
         node-version:
           - 14
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index db41ad3007..af32008400 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -21,7 +21,7 @@ jobs:
           - 5.2.x
           - 5.1.x
           - 5.0.x
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda
           - 4.14.x
         apron:
           - false
@@ -92,7 +92,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
     name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade)
 
@@ -133,7 +133,7 @@ jobs:
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
         # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.5)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.2+options ocaml-option-flambda num.1.5)
 
       - name: Build
         run: ./make.sh nat
@@ -190,7 +190,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
     runs-on: ${{ matrix.os }}
 
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 410d363ac8..26f8bb53e7 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -71,12 +71,12 @@ depends: [
   "logs" {= "0.7.0"}
   "mlgmpidl" {= "1.3.0"}
   "num" {= "1.5"}
-  "ocaml" {= "4.14.0"}
+  "ocaml" {= "4.14.2"}
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocaml-config" {= "2"}
   "ocaml-option-flambda" {= "1"}
   "ocaml-syntax-shims" {= "1.0.0"}
-  "ocaml-variants" {= "4.14.0+options"}
+  "ocaml-variants" {= "4.14.2+options"}
   "ocamlbuild" {= "0.14.3"}
   "ocamlfind" {= "1.9.6"}
   "odoc" {= "2.4.2" & with-doc}
diff --git a/gobview b/gobview
index 287bf59be9..4069f32f82 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 287bf59be9e25ceea704384c65e0d91565bb749d
+Subproject commit 4069f32f82efdefb43c970fb77ca29671a4b6972
diff --git a/make.sh b/make.sh
index 5b55e51beb..0f76759065 100755
--- a/make.sh
+++ b/make.sh
@@ -8,7 +8,7 @@ opam_setup() {
   set -x
   opam init -y -a --bare $SANDBOXING # sandboxing is disabled in travis and docker
   opam update
-  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda --locked
+  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda --locked
 }
 
 rule() {

From 14e5523ce2b49eed48ec72837d9a41eff4b0f3e3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 27 Jun 2024 11:40:07 +0300
Subject: [PATCH 12/34] Remove small margin for Apron domain show

---
 src/cdomains/apron/apronDomain.apron.ml | 2 +-
 src/common/util/gobFormat.ml            | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d0ef268ca6..26e954f1b2 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -442,7 +442,7 @@ struct
   let invariant _ = []
 
   let show (x:t) =
-    Format.asprintf "%a (env: %a)" A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)
+    Format.asprintf "%t%a (env: %a)" GobFormat.pp_set_infinite_geometry A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)
   let pretty () (x:t) = text (show x)
 
   let equal x y =
diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml
index 3cda0a4758..1b4d28a26c 100644
--- a/src/common/util/gobFormat.ml
+++ b/src/common/util/gobFormat.ml
@@ -19,3 +19,7 @@ let pp_set_ansi_color_tags ppf =
   Format.pp_set_mark_tags ppf true
 
 let pp_print_nothing (ppf: Format.formatter) () = ()
+
+let pp_infinity = 1000000001 (* Exact value not exposed before OCaml 5.2, but use the smallest value permitted by documentation. *)
+
+let pp_set_infinite_geometry = Format.pp_set_geometry ~max_indent:(pp_infinity - 2) ~margin:(pp_infinity - 1)

From d2527b7f757e486cadfd551c712796cc6ee4c1b2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 27 Jun 2024 11:49:10 +0300
Subject: [PATCH 13/34] Add Printable.SimpleFormat

---
 src/common/domains/printable.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index 1a642c932a..b6b1dc5c3a 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -88,6 +88,20 @@ struct
   let to_yojson x = `String (show x)
 end
 
+module type Formatable =
+sig
+  type t
+  val pp: Format.formatter -> t -> unit
+end
+
+module SimpleFormat (P: Formatable) =
+struct
+  let show x = Format.asprintf "%t%a" GobFormat.pp_set_infinite_geometry P.pp x
+  let pretty () x = text (show x)
+  let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
+  let to_yojson x = `String (show x)
+end
+
 
 module type Name = sig val name: string end
 module UnitConf (N: Name) =

From 6269d1e2942b8567601a30d35657beadeaabecaa Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 27 Jun 2024 12:02:59 +0300
Subject: [PATCH 14/34] Add some Printables to GobApron

---
 .../apron/affineEqualityDomain.apron.ml       |  3 +-
 src/cdomains/apron/apronDomain.apron.ml       | 18 +++---
 src/cdomains/apron/gobApron.apron.ml          | 56 ++++++++++++++++++-
 .../apron/linearTwoVarEqualityDomain.apron.ml |  6 +-
 src/cdomains/apron/sharedFunctions.apron.ml   |  2 +-
 5 files changed, 68 insertions(+), 17 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 7e60cce74b..6bef6c329e 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -206,8 +206,7 @@ struct
       Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]")
 
   let pretty () (x:t) = text (show x)
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
-
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
   let name () = "affeq"
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 26e954f1b2..826eec0715 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -283,7 +283,7 @@ struct
   let assign_exp_with ask nd v e no_ov =
     match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with
     | texpr1 ->
-      if M.tracing then M.trace "apron" "assign_exp converted: %s" (Format.asprintf "%a" Texpr1.print texpr1);
+      if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pretty texpr1;
       A.assign_texpr_with Man.mgr nd v texpr1 None
     | exception Convert.Unsupported_CilExp _ ->
       if M.tracing then M.trace "apron" "assign_exp unsupported";
@@ -442,7 +442,7 @@ struct
   let invariant _ = []
 
   let show (x:t) =
-    Format.asprintf "%t%a (env: %a)" GobFormat.pp_set_infinite_geometry A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)
+    Format.asprintf "%t%a (env: %a)" GobFormat.pp_set_infinite_geometry A.print x Environment.pp (A.env x)
   let pretty () (x:t) = text (show x)
 
   let equal x y =
@@ -454,7 +454,7 @@ struct
   let compare (x:t) y: int =
     (* there is no A.compare, but polymorphic compare should delegate to Abstract0 and Environment compare's implemented in Apron's C *)
     Stdlib.compare x y
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)))
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) Environment.printXml (A.env x)
 
   let to_yojson (x: t) =
     let constraints =
@@ -463,11 +463,9 @@ struct
       |> Lincons1Set.elements
       |> List.map (fun lincons1 -> `String (Lincons1.show lincons1))
     in
-    let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))
-    in
     `Assoc [
       ("constraints", `List constraints);
-      ("env", env);
+      ("env", Environment.to_yojson (A.env x));
     ]
 
   let unify x y =
@@ -533,9 +531,9 @@ struct
     | _ ->
       begin match Convert.tcons1_of_cil_exp ask d (A.env d) e negate no_ov with
         | tcons1 ->
-          if M.tracing then M.trace "apron" "assert_constraint %a %s" d_exp e (Format.asprintf "%a" Tcons1.print tcons1);
+          if M.tracing then M.trace "apron" "assert_constraint %a %a" d_exp e Tcons1.pretty tcons1;
           if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d;
-          if M.tracing then M.trace "apron" "assert_constraint tcons1: %s" (Format.asprintf "%a" Tcons1.print tcons1);
+          if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1;
           let r = meet_tcons ask d tcons1 e in
           if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r;
           r
@@ -598,7 +596,7 @@ struct
     let x_cons = A.to_lincons_array Man.mgr x_j in
     let y_cons = A.to_lincons_array Man.mgr y_j in
     let try_add_con j con1 =
-      if M.tracing then M.tracei "apron" "try_add_con %s" (Format.asprintf "%a" (Lincons1.print: Format.formatter -> Lincons1.t -> unit) con1);
+      if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pretty con1;
       let t = meet_lincons j con1 in
       let t_x = A.change_environment Man.mgr t x_env false in
       let t_y = A.change_environment Man.mgr t y_env false in
@@ -637,7 +635,7 @@ struct
       in
       let env_exists_mem_con1 env con1 =
         let r = env_exists_mem_con1 env con1 in
-        if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r;
+        if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pretty env Lincons1.pretty con1 r;
         r
       in
       (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *)
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index e202a88c60..f2322c1473 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -18,7 +18,14 @@ module Lincons1 =
 struct
   include Lincons1
 
-  let show = Format.asprintf "%a" print
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
   let compare x y = String.compare (show x) (show y) (* HACK *)
 
   let num_vars x =
@@ -43,12 +50,59 @@ struct
     |> of_enum
 end
 
+module Texpr1 =
+struct
+  include Texpr1
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
+  module Expr =
+  struct
+    type t = expr
+
+    let pp = print_expr
+    include Printable.SimpleFormat (
+      struct
+        type nonrec t = t
+        let pp = pp
+      end
+      )
+  end
+end
+
+module Tcons1 =
+struct
+  include Tcons1
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+end
+
 (** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain.
     A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *)
 module Environment =
 struct
   include Environment
 
+  let pp: Format.formatter -> Environment.t -> unit = Environment.print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
   let ivars_only env =
     let ivs, fvs = Environment.vars env in
     assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index 5558bc2c96..fa71e3d1a5 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -11,7 +11,7 @@ open Batteries
 open GoblintCil
 open Pretty
 module M = Messages
-open Apron
+open GobApron
 open VectorMatrix
 
 module Mpqf = SharedFunctions.Mpqf
@@ -331,7 +331,7 @@ struct
 
   let simplified_monomials_from_texp (t: t) texp =
     let res = simplified_monomials_from_texp t texp in
-    if M.tracing then M.tracel "from_texp" "%s %s -> %s" (EConj.show @@ snd @@ BatOption.get t.d) (Format.asprintf "%a" Texpr1.print_expr texp)
+    if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
         (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);
     res
 
@@ -424,7 +424,7 @@ struct
         EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
 
   let pretty () (x:t) = text (show x)
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
   let meet_with_one_conj t i (var, o, divi) =
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 8c94c996b0..9627b4762a 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -196,7 +196,7 @@ struct
     in
     let exp = Cil.constFold false exp in
     let res = conv exp in
-    if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %s (%b)" d_plainexp exp (Format.asprintf "%a" Texpr1.print_expr res) (Lazy.force no_ov);
+    if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
     res
 
   let texpr1_of_cil_exp ask d env e no_ov =

From e37b7d756ee7f0fcd4a8f56ded7f01adf89d090f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 27 Jun 2024 12:06:04 +0300
Subject: [PATCH 15/34] Remove pointless `Format.asprintf "%s"`

---
 src/cdomains/apron/affineEqualityDomain.apron.ml       | 4 ++--
 src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 6bef6c329e..8bb99f2264 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -203,10 +203,10 @@ struct
     | Some m when Matrix.is_empty m -> "⊤"
     | Some m ->
       let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in
-      Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]")
+      "[|"^ (String.concat "; " constraint_list) ^"|]"
 
   let pretty () (x:t) = text (show x)
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) Environment.printXml x.env
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
   let name () = "affeq"
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index fa71e3d1a5..bd6b81402a 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -424,7 +424,7 @@ struct
         EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
 
   let pretty () (x:t) = text (show x)
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) Environment.printXml x.env
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
   let meet_with_one_conj t i (var, o, divi) =

From 5ea925eab57750f77acad4081dc6d46d6016814d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 27 Jun 2024 12:28:09 +0300
Subject: [PATCH 16/34] Extract GobFormat.asprintf

---
 src/cdomains/apron/apronDomain.apron.ml | 4 ++--
 src/common/domains/printable.ml         | 2 +-
 src/common/util/gobFormat.ml            | 5 +++++
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 826eec0715..777db5a297 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -442,7 +442,7 @@ struct
   let invariant _ = []
 
   let show (x:t) =
-    Format.asprintf "%t%a (env: %a)" GobFormat.pp_set_infinite_geometry A.print x Environment.pp (A.env x)
+    GobFormat.asprintf "%a (env: %a)" A.print x Environment.pp (A.env x)
   let pretty () (x:t) = text (show x)
 
   let equal x y =
@@ -454,7 +454,7 @@ struct
   let compare (x:t) y: int =
     (* there is no A.compare, but polymorphic compare should delegate to Abstract0 and Environment compare's implemented in Apron's C *)
     Stdlib.compare x y
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) Environment.printXml (A.env x)
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (GobFormat.asprint A.print x)) Environment.printXml (A.env x)
 
   let to_yojson (x: t) =
     let constraints =
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index b6b1dc5c3a..ee0eda0766 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -96,7 +96,7 @@ end
 
 module SimpleFormat (P: Formatable) =
 struct
-  let show x = Format.asprintf "%t%a" GobFormat.pp_set_infinite_geometry P.pp x
+  let show x = GobFormat.asprint P.pp x
   let pretty () x = text (show x)
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
   let to_yojson x = `String (show x)
diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml
index 1b4d28a26c..8f26ff0087 100644
--- a/src/common/util/gobFormat.ml
+++ b/src/common/util/gobFormat.ml
@@ -23,3 +23,8 @@ let pp_print_nothing (ppf: Format.formatter) () = ()
 let pp_infinity = 1000000001 (* Exact value not exposed before OCaml 5.2, but use the smallest value permitted by documentation. *)
 
 let pp_set_infinite_geometry = Format.pp_set_geometry ~max_indent:(pp_infinity - 2) ~margin:(pp_infinity - 1)
+
+let asprintf (fmt: ('a, Format.formatter, unit, string) format4): 'a =
+  Format.asprintf ("%t" ^^ fmt) pp_set_infinite_geometry
+
+let asprint pp x = asprintf "%a" pp x (* eta-expanded to bypass value restriction *)

From 71a1657124fd4f9fb12e954f199189f8ef6e5244 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 5 Jul 2024 13:09:03 +0300
Subject: [PATCH 17/34] Remove apron v0.9.15 pin

---
 goblint.opam          | 1 -
 goblint.opam.locked   | 4 ----
 goblint.opam.template | 1 -
 3 files changed, 6 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index ec6a1f8fcb..0cc5eab3a2 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -84,7 +84,6 @@ pin-depends: [
   [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#b3172bd51e4bb0135716a300cab424a56970d96f" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 8b184e189d..532b8e1aff 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -140,9 +140,5 @@ pin-depends: [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
   ]
-  [
-    "apron.v0.9.15"
-    "git+https://github.com/antoinemine/apron.git#b3172bd51e4bb0135716a300cab424a56970d96f"
-  ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
diff --git a/goblint.opam.template b/goblint.opam.template
index 27be21015f..2d5ef10bc9 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -6,7 +6,6 @@ pin-depends: [
   [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#b3172bd51e4bb0135716a300cab424a56970d96f" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

From a23b728a4023b9c8582c852b7f6d31ceb4f8b328 Mon Sep 17 00:00:00 2001
From: Fabian Stemmler <stemmler@in.tum.de>
Date: Thu, 11 Jul 2024 11:29:39 +0200
Subject: [PATCH 18/34] propagate bottom through narrowing operator of lifters

---
 src/domain/lattice.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
index 99322c09d8..d45ddcbfc2 100644
--- a/src/domain/lattice.ml
+++ b/src/domain/lattice.ml
@@ -277,6 +277,8 @@ struct
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
     | _ -> x
 end
 
@@ -337,6 +339,8 @@ struct
     | (`Lifted x, `Lifted y) ->
       (try `Lifted (Base.narrow x y)
        with Uncomparable -> `Bot)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
     | _ -> x
 end
 
@@ -408,6 +412,8 @@ struct
     match (x,y) with
     | (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.narrow x y)
     | (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.narrow x y)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
     | _ -> x
 
 end
@@ -539,6 +545,7 @@ struct
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (_, `Bot) -> `Bot
     | _ -> x
 end
 
@@ -580,6 +587,7 @@ struct
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (`Top, y) -> y
     | _ -> x
 
   let pretty_diff () (x,y) =

From 11ed4180e3064e4d43fb01751df553e233235a77 Mon Sep 17 00:00:00 2001
From: Jonas August <ge59duv@mytum.de>
Date: Thu, 29 Jun 2023 08:29:30 +0200
Subject: [PATCH 19/34] Fix depreciated option

---
 tests/regression/46-apron2/26-autotune.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/46-apron2/26-autotune.c b/tests/regression/46-apron2/26-autotune.c
index 96c5c85278..ec8f55fe19 100644
--- a/tests/regression/46-apron2/26-autotune.c
+++ b/tests/regression/46-apron2/26-autotune.c
@@ -1,4 +1,4 @@
-//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
+//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
 // Check that autotuner disables context for apron as well for recursive calls
 #include <goblint.h>
 

From 0077e1d78857f238aae4fb87a0d7b0ef5aba5b9c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 16 Jul 2024 15:09:51 +0300
Subject: [PATCH 20/34] Replace --sets with --set in tests

---
 scripts/creduce/privPrecCompare.sh                       | 2 +-
 scripts/privPrecCompare.sh                               | 2 +-
 tests/regression/01-cpa/71-widen-sides.c                 | 2 +-
 tests/regression/46-apron2/03-other-assume.c             | 2 +-
 tests/regression/46-apron2/04-other-assume-inprec.c      | 2 +-
 tests/regression/46-apron2/30-autotune-stub.c            | 2 +-
 tests/regression/58-base-mm-tid/01-tid-toy1.c            | 2 +-
 tests/regression/58-base-mm-tid/22-other-assume.c        | 2 +-
 tests/regression/58-base-mm-tid/23-other-assume-inprec.c | 2 +-
 tests/regression/66-interval-set-one/51-widen-sides.c    | 2 +-
 10 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/scripts/creduce/privPrecCompare.sh b/scripts/creduce/privPrecCompare.sh
index fdc5f9219d..2165112924 100755
--- a/scripts/creduce/privPrecCompare.sh
+++ b/scripts/creduce/privPrecCompare.sh
@@ -22,7 +22,7 @@ for PRIV in "${PRIVS[@]}"; do
     PRIVDUMP="$OUTDIR/$PRIV"
     LOG="$OUTDIR/$PRIV.log"
     rm -f $PRIVDUMP
-    $GOBLINTDIR/goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
+    $GOBLINTDIR/goblint --set exp.privatization $PRIV --set exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
     grep -F "Function definition missing" $LOG && exit 1
 done
 
diff --git a/scripts/privPrecCompare.sh b/scripts/privPrecCompare.sh
index c5b9f2c01e..2b09fb80b5 100755
--- a/scripts/privPrecCompare.sh
+++ b/scripts/privPrecCompare.sh
@@ -10,7 +10,7 @@ mkdir -p $OUTDIR
 for PRIV in "${PRIVS[@]}"; do
     echo $PRIV
     PRIVDUMP="$OUTDIR/$PRIV"
-    ./goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP "$@"
+    ./goblint --set exp.privatization $PRIV --set exp.priv-prec-dump $PRIVDUMP "$@"
 done
 
 PRIVDUMPS=("${PRIVS[*]/#/$OUTDIR/}") # why [*] here?
diff --git a/tests/regression/01-cpa/71-widen-sides.c b/tests/regression/01-cpa/71-widen-sides.c
index 522f6fae44..a93124c6e5 100644
--- a/tests/regression/01-cpa/71-widen-sides.c
+++ b/tests/regression/01-cpa/71-widen-sides.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval --sets solvers.td3.side_widen sides-local
+// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval --set solvers.td3.side_widen sides-local
 #include <goblint.h>
 
 int further(int n) {
diff --git a/tests/regression/46-apron2/03-other-assume.c b/tests/regression/46-apron2/03-other-assume.c
index 635911a197..c136d1bde3 100644
--- a/tests/regression/46-apron2/03-other-assume.c
+++ b/tests/regression/46-apron2/03-other-assume.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.relation.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/04-other-assume-inprec.c b/tests/regression/46-apron2/04-other-assume-inprec.c
index 09b8d150a8..ccf8ecefa1 100644
--- a/tests/regression/46-apron2/04-other-assume-inprec.c
+++ b/tests/regression/46-apron2/04-other-assume-inprec.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.relation.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/30-autotune-stub.c b/tests/regression/46-apron2/30-autotune-stub.c
index e1b7603c3b..02c80e7d21 100644
--- a/tests/regression/46-apron2/30-autotune-stub.c
+++ b/tests/regression/46-apron2/30-autotune-stub.c
@@ -1,4 +1,4 @@
-//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
+//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
 // Check that autotuner respect goblint_stub attributes as hints to not track variables.
 #include <goblint.h>
 
diff --git a/tests/regression/58-base-mm-tid/01-tid-toy1.c b/tests/regression/58-base-mm-tid/01-tid-toy1.c
index bc3cd18efa..49e96881d1 100644
--- a/tests/regression/58-base-mm-tid/01-tid-toy1.c
+++ b/tests/regression/58-base-mm-tid/01-tid-toy1.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid
 // Inspired by 36/71
 #include <pthread.h>
 #include <goblint.h>
diff --git a/tests/regression/58-base-mm-tid/22-other-assume.c b/tests/regression/58-base-mm-tid/22-other-assume.c
index 4f5c73b038..301195ac1f 100644
--- a/tests/regression/58-base-mm-tid/22-other-assume.c
+++ b/tests/regression/58-base-mm-tid/22-other-assume.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid
 // Copy of 46/03 for base
 #include <pthread.h>
 #include <goblint.h>
diff --git a/tests/regression/58-base-mm-tid/23-other-assume-inprec.c b/tests/regression/58-base-mm-tid/23-other-assume-inprec.c
index 37e59d3edf..a4bac04c59 100644
--- a/tests/regression/58-base-mm-tid/23-other-assume-inprec.c
+++ b/tests/regression/58-base-mm-tid/23-other-assume-inprec.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins
 // Copy of 46/04 for base
 #include <pthread.h>
 #include <goblint.h>
diff --git a/tests/regression/66-interval-set-one/51-widen-sides.c b/tests/regression/66-interval-set-one/51-widen-sides.c
index b086baf026..53fe749704 100644
--- a/tests/regression/66-interval-set-one/51-widen-sides.c
+++ b/tests/regression/66-interval-set-one/51-widen-sides.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval_set --sets solvers.td3.side_widen sides-local
+// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval_set --set solvers.td3.side_widen sides-local
 #include <goblint.h>
 
 int further(int n) {

From 67c18668154d79ce5cdd71c887788c8cfa09aab0 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 8 Dec 2023 14:26:31 +0100
Subject: [PATCH 21/34] change may fail to fail annotation

---
 tests/regression/36-apron/86-branched-thread-creation.c         | 2 +-
 tests/regression/58-base-mm-tid/15-branched-thread-creation.c   | 2 +-
 .../67-interval-sets-two/16-branched-thread-creation.c          | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/regression/36-apron/86-branched-thread-creation.c b/tests/regression/36-apron/86-branched-thread-creation.c
index cac0a881a6..91a5411e8f 100644
--- a/tests/regression/36-apron/86-branched-thread-creation.c
+++ b/tests/regression/36-apron/86-branched-thread-creation.c
@@ -40,7 +40,7 @@ int main(void) {
 
   if(!mt) {
     pthread_mutex_lock(&mutex);
-    __goblint_check(g==h); //MAYFAIL
+    __goblint_check(g==h); //FAIL
     pthread_mutex_unlock(&mutex);
   }
 
diff --git a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c
index 3292182adc..c7bb43519f 100644
--- a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c
+++ b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c
@@ -41,7 +41,7 @@ int main(void) {
 
   if(!mt) {
     pthread_mutex_lock(&mutex);
-    __goblint_check(g==h); //MAYFAIL
+    __goblint_check(g==h); //FAIL
     pthread_mutex_unlock(&mutex);
   }
 
diff --git a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c
index c309ec8ffd..d97f800621 100644
--- a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c
+++ b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c
@@ -41,7 +41,7 @@ int main(void) {
 
   if(!mt) {
     pthread_mutex_lock(&mutex);
-    __goblint_check(g==h); //MAYFAIL
+    __goblint_check(g==h); //FAIL
     pthread_mutex_unlock(&mutex);
   }
 

From f1c6e2c6d4acf94a2137433d34364c8c639c9aec Mon Sep 17 00:00:00 2001
From: J2000A <email@jonasaugust.de>
Date: Fri, 5 May 2023 14:41:52 +0200
Subject: [PATCH 22/34] Adjust evalAssert to offer __goblint_check(exp) with
 the option trans.goblint-check

---
 src/config/options.schema.json | 6 ++++++
 src/transform/evalAssert.ml    | 7 +++++--
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index d259a6f418..2e2a9212ef 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1561,6 +1561,12 @@
           "description": "Output filename for transformations that output a transformed file.",
           "type":"string",
           "default": "transformed.c"
+        },
+        "goblint-check" : {
+          "title": "trans.goblint-check",
+          "description": "Write __Goblint_Check(exp) in the file instead of __VERIFIER_assert(exp).",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index eab06222ef..82b92b9040 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -26,8 +26,11 @@ module EvalAssert = struct
   (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
   let surroundByAtomic = true
 
+  (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp)*)
+  let goblintCheck = GobConfig.get_bool "trans.goblint-check"
+
   (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass = makeVarinfo true "__VERIFIER_assert" (TVoid [])
+  let ass = if goblintCheck then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid [])
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -60,7 +63,7 @@ module EvalAssert = struct
         | `Lifted e ->
           let es = WitnessUtil.InvariantExp.process_exp e in
           let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv ass); ("exp", Fe e)]) es in
-          if surroundByAtomic then
+          if surroundByAtomic && not goblintCheck then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
             let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in
             abegin :: (asserts @ [aend])

From 8db9e1d320de69baf396bab7b56f55149f577a69 Mon Sep 17 00:00:00 2001
From: Jonas August <ge59duv@mytum.de>
Date: Wed, 10 May 2023 19:24:34 +0200
Subject: [PATCH 23/34] Adopt evalAssert.ml so the option is checked correctly
 at runtime

---
 src/transform/evalAssert.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 82b92b9040..fb9cf84d86 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -26,11 +26,6 @@ module EvalAssert = struct
   (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
   let surroundByAtomic = true
 
-  (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp)*)
-  let goblintCheck = GobConfig.get_bool "trans.goblint-check"
-
-  (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass = if goblintCheck then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid [])
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -41,6 +36,8 @@ module EvalAssert = struct
     (* TODO: handle witness.invariant.loop-head *)
     val emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock"
     val emit_other = GobConfig.get_bool "witness.invariant.other"
+    (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *)
+    val goblintCheck = GobConfig.get_bool "trans.goblint-check"
 
     method! vstmt s =
       let is_lock exp args =
@@ -53,6 +50,10 @@ module EvalAssert = struct
         | _ -> false
       in
 
+      (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
+      (* Moved in method because Options can not be checked in the module *)
+      let ass = if goblintCheck then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid []) in
+
       let make_assert ~node loc lval =
         let lvals = match lval with
           | None -> Lval.Set.top ()

From 21d804a0a1ea9337075be413d30ec02cdfd5e274 Mon Sep 17 00:00:00 2001
From: Jonas August <ge59duv@mytum.de>
Date: Tue, 16 May 2023 18:00:31 +0200
Subject: [PATCH 24/34] Fix Goblint Option Retrieving by adding Unit to
 constant

---
 src/transform/evalAssert.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index fb9cf84d86..7fc70531db 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -26,6 +26,11 @@ module EvalAssert = struct
   (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
   let surroundByAtomic = true
 
+  (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *)
+  let goblintCheck () = GobConfig.get_bool "trans.goblint-check"
+
+  (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
+  let ass () = if goblintCheck then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid []) in
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -36,8 +41,6 @@ module EvalAssert = struct
     (* TODO: handle witness.invariant.loop-head *)
     val emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock"
     val emit_other = GobConfig.get_bool "witness.invariant.other"
-    (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *)
-    val goblintCheck = GobConfig.get_bool "trans.goblint-check"
 
     method! vstmt s =
       let is_lock exp args =
@@ -50,10 +53,6 @@ module EvalAssert = struct
         | _ -> false
       in
 
-      (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-      (* Moved in method because Options can not be checked in the module *)
-      let ass = if goblintCheck then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid []) in
-
       let make_assert ~node loc lval =
         let lvals = match lval with
           | None -> Lval.Set.top ()

From 69a33364e018a4aaea787b8aa4bda58441bd5b41 Mon Sep 17 00:00:00 2001
From: Jonas August <ge59duv@mytum.de>
Date: Tue, 23 May 2023 20:48:36 +0200
Subject: [PATCH 25/34] Bugfix

---
 src/transform/evalAssert.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 7fc70531db..56f3d5eb5f 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -30,7 +30,7 @@ module EvalAssert = struct
   let goblintCheck () = GobConfig.get_bool "trans.goblint-check"
 
   (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass () = if goblintCheck then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid []) in
+  let ass () = if goblintCheck () then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid [])
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -62,8 +62,8 @@ module EvalAssert = struct
         match (ask ~node loc).f (Queries.Invariant context) with
         | `Lifted e ->
           let es = WitnessUtil.InvariantExp.process_exp e in
-          let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv ass); ("exp", Fe e)]) es in
-          if surroundByAtomic && not goblintCheck then
+          let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv (ass ())); ("exp", Fe e)]) es in
+          if surroundByAtomic && not (goblintCheck ()) then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
             let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in
             abegin :: (asserts @ [aend])

From 3e3c1ebda3871a079fbbe65c4b84828fdbbfc914 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 8 Dec 2023 14:37:44 +0100
Subject: [PATCH 26/34] rename option

---
 src/config/options.schema.json | 18 +++++++++++++-----
 src/transform/evalAssert.ml    |  2 +-
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 2e2a9212ef..d808f121c3 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1562,11 +1562,19 @@
           "type":"string",
           "default": "transformed.c"
         },
-        "goblint-check" : {
-          "title": "trans.goblint-check",
-          "description": "Write __Goblint_Check(exp) in the file instead of __VERIFIER_assert(exp).",
-          "type": "boolean",
-          "default": false
+        "assert" : {
+          "title": "trans.assert",
+          "type": "object",
+          "properties": {
+            "goblint-check": {
+              "title": "trans.assert.goblint-check",
+              "description":
+                "Write __goblint_check(exp) in the file instead of __VERIFIER_assert(exp).",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 56f3d5eb5f..94fdfb8602 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -27,7 +27,7 @@ module EvalAssert = struct
   let surroundByAtomic = true
 
   (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *)
-  let goblintCheck () = GobConfig.get_bool "trans.goblint-check"
+  let goblintCheck () = GobConfig.get_bool "trans.assert.goblint-check"
 
   (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
   let ass () = if goblintCheck () then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid [])

From cae69f7006fa7c2f481e48d8613bc4f62a40b466 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 16 Jul 2024 15:46:32 +0300
Subject: [PATCH 27/34] Refactor trans.assert options

---
 src/config/options.schema.json | 16 +++++++++++-----
 src/transform/evalAssert.ml    | 20 +++++++++-----------
 2 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index d808f121c3..0cb1b6ee67 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1566,12 +1566,18 @@
           "title": "trans.assert",
           "type": "object",
           "properties": {
-            "goblint-check": {
-              "title": "trans.assert.goblint-check",
-              "description":
-                "Write __goblint_check(exp) in the file instead of __VERIFIER_assert(exp).",
+            "function": {
+              "title": "trans.assert.function",
+              "description": "Function to use for assertions in output.",
+              "type": "string",
+              "enum": ["assert", "__goblint_check", "__VERIFIER_assert"],
+              "default": "__VERIFIER_assert"
+            },
+            "wrap-atomic": {
+              "title": "trans.assert.wrap-atomic",
+              "description": "Wrap assertions in __VERIFIER_atomic_begin and __VERIFIER_atomic_end.",
               "type": "boolean",
-              "default": false
+              "default": true
             }
           },
           "additionalProperties": false
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 94fdfb8602..0fee26355b 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -22,15 +22,8 @@ open Formatcil
         will be removed and they will fail on the next iteration
 *)
 
-module EvalAssert = struct
-  (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
-  let surroundByAtomic = true
-
-  (* variable for generating __goblint_check(exp) instead of __VERIFIER_assert(exp) *)
-  let goblintCheck () = GobConfig.get_bool "trans.assert.goblint-check"
-
-  (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass () = if goblintCheck () then makeVarinfo true "__goblint_check" (TVoid []) else makeVarinfo true "__VERIFIER_assert" (TVoid [])
+module EvalAssert =
+struct
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -42,6 +35,11 @@ module EvalAssert = struct
     val emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock"
     val emit_other = GobConfig.get_bool "witness.invariant.other"
 
+    (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
+    val assert_function = makeVarinfo true (GobConfig.get_string "trans.assert.function") (TVoid [])
+    (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
+    val surroundByAtomic = GobConfig.get_bool "trans.assert.wrap-atomic"
+
     method! vstmt s =
       let is_lock exp args =
         match exp with
@@ -62,8 +60,8 @@ module EvalAssert = struct
         match (ask ~node loc).f (Queries.Invariant context) with
         | `Lifted e ->
           let es = WitnessUtil.InvariantExp.process_exp e in
-          let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv (ass ())); ("exp", Fe e)]) es in
-          if surroundByAtomic && not (goblintCheck ()) then
+          let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe e)]) es in
+          if surroundByAtomic then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
             let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in
             abegin :: (asserts @ [aend])

From 14d51d51fe952f6edad9871350f71cfccaea710d Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 12 Jul 2024 16:58:31 +0200
Subject: [PATCH 28/34] Check overflows when generating witnesses

---
 src/cdomains/apron/sharedFunctions.apron.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 4809e97917..a9406d48e9 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -274,7 +274,7 @@ struct
     let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in
     let append_summand (c:Coeff.union_5) v =
       match V.to_cil_varinfo v with
-      | Some vinfo ->
+      | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
         (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *)
         let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
         let coeff, flip = coeff_to_const true c in
@@ -284,6 +284,7 @@ struct
         else
           expr := BinOp(PlusA,!expr,prod,longlong)
       | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s"  (Var.to_string v); raise Unsupported_Linexpr1
+      | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %s"  (Var.to_string v); raise Unsupported_Linexpr1
     in
     Linexpr1.iter append_summand linexpr1;
     !expr

From 726725b88015547e9aeab38232fe130ab113993f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 17 Jul 2024 11:15:45 +0300
Subject: [PATCH 29/34] Add Printable functions to GobApron.Var

---
 src/analyses/apron/relationAnalysis.apron.ml  |  4 +--
 .../apron/affineEqualityDomain.apron.ml       | 10 +++---
 src/cdomains/apron/gobApron.apron.ml          |  9 ++++++
 .../apron/linearTwoVarEqualityDomain.apron.ml | 32 +++++++++----------
 src/cdomains/apron/sharedFunctions.apron.ml   |  4 +--
 5 files changed, 34 insertions(+), 25 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index a42d78d71a..6dd2a65cee 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -295,7 +295,7 @@ struct
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
-    let vname = Apron.Var.to_string var in
+    let vname = GobApron.Var.show var in
     let locals = fundec.sformals @ fundec.slocals in
     match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true
@@ -418,7 +418,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
+    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pretty ())) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 8bb99f2264..ec0bb9b940 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -181,7 +181,7 @@ struct
             else if Z.lt coeff Z.minus_one then Z.to_string coeff
             else Format.asprintf "+%s" (Z.to_string coeff)
           in
-          coeff_str ^ Var.to_string var
+          coeff_str ^ Var.show var
       in
       let const_to_str vl =
         if Z.equal vl Z.zero then
@@ -429,8 +429,8 @@ struct
 
   let assign_exp ask t var exp no_ov =
     let res = assign_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s"
-        (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
+    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s"
+        (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res);
     res
 
   let assign_var (t: VarManagement(Vc)(Mx).t) v v' =
@@ -440,7 +440,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ;
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
     res
 
   let assign_var_parallel t vv's =
@@ -498,7 +498,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index f2322c1473..fca28ff8f0 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -11,6 +11,15 @@ end
 module Var =
 struct
   include Var
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
   let equal x y = Var.compare x y = 0
 end
 
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index bd6b81402a..c13aca60ea 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -158,7 +158,7 @@ module EqualitiesConjunction = struct
             let (newref,offs,divi) = (get_rhs d head) in
             let (coeff,y) = BatOption.get newref in
             let (y,yrhs) = inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *)
-            let shifted_cluster =  (List.fold (fun map i -> 
+            let shifted_cluster =  (List.fold (fun map i ->
                 let irhs = (get_rhs d i) in (* old entry is i = irhs *)
                 Rhs.subst yrhs y irhs |>    (* new entry for i is irhs [yrhs/y] *)
                 set_rhs map i
@@ -222,7 +222,7 @@ module EqualitiesConjunction = struct
        | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)->
          (match get_rhs ts j with
           (* ts[x_j]=o2/d2             ========>  ... *)
-          | (None            , o2, divi2) -> 
+          | (None            , o2, divi2) ->
             let newxi  = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in
             let newxh1 = snd @@ inverse i (coeff1,h1,o1,divi1) in
             let newxh1 = Rhs.subst newxi i newxh1 in
@@ -251,7 +251,7 @@ module EqualitiesConjunction = struct
     else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *)
       (* so now, we transform with the inverse of the transformer: *)
       let inv = snd (inverse i (coeff,j,offs,divi)) in
-      IntMap.fold (fun k v acc -> 
+      IntMap.fold (fun k v acc ->
           match v with
           | (Some (c,x),o,d) when x=i-> set_rhs acc k (Rhs.subst inv i v)
           | _ -> acc
@@ -281,7 +281,7 @@ struct
     let multiply a b =
       (* if one of them is a constant, then multiply. Otherwise, the expression is not linear *)
       match a, b with
-      | [(None,coeff, divi)], c 
+      | [(None,coeff, divi)], c
       | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c
       | _ -> raise NotLinearExpr
     in
@@ -314,7 +314,7 @@ struct
     | x -> Some(x)
 
   (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *)
-  let simplified_monomials_from_texp (t: t) texp = 
+  let simplified_monomials_from_texp (t: t) texp =
     BatOption.bind (monomials_from_texp t texp)
       (fun monomiallist ->
          let d = Option.get t.d in
@@ -323,7 +323,7 @@ struct
            | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)
            | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConj.get_rhs d idx) idx (v,offs,divi) in (* normalize! *)
              let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in
-             let gcdee = Z.gcd adiv divi in 
+             let gcdee = Z.gcd adiv divi in
              (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi))
          in
          let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *)
@@ -339,7 +339,7 @@ struct
     BatOption.bind (simplified_monomials_from_texp t texp )
       (fun (sum_of_terms, (constant,divisor)) ->
          (match sum_of_terms with
-          | [] -> Some (None, constant,divisor) 
+          | [] -> Some (None, constant,divisor)
           | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi))
           |_ -> None))
 
@@ -447,7 +447,7 @@ struct
     let t1 = change_d t1 sup_env ~add:true ~del:false in
     let t2 = change_d t2 sup_env ~add:true ~del:false in
     match t1.d, t2.d with
-    | Some d1', Some d2' -> 
+    | Some d1', Some d2' ->
       EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*)
     | _ -> {d = None; env = sup_env}
 
@@ -489,7 +489,7 @@ struct
          - lhs itself
          - criteria A and B that characterize equivalence class, depending on the reference variable and the affine expression parameters wrt. each EConj
          - rhs1
-         - rhs2 
+         - rhs2
            however, we have to account for the sparseity of EConj maps by manually patching holes with default values *)
       let joinfunction lhs rhs1 rhs2 =
         (
@@ -516,15 +516,15 @@ struct
       let varentry ci offi ch offh xh =
         let (coeff,off,d) = Q.(ci,(offi*ch)-(ci*offh),ch) in (* compute new rhs in Q *)
         let (coeff,off,d) = Z.(coeff.num*d.den*off.den,off.num*d.den*coeff.den,d. num*coeff.den*off.den) in (* convert that back into Z *)
-        Rhs.canonicalize (Some(coeff,xh),off,d) 
+        Rhs.canonicalize (Some(coeff,xh),off,d)
       in
       (* ci1 = a*ch1+b /\ ci2 = a*ch2+b *)
       (* ===> a = (ci1-ci2)/(ch1-ch2) b = ci2-a*ch2 *)
-      let constentry ci1 ci2 ch1 ch2 xh = 
+      let constentry ci1 ci2 ch1 ch2 xh =
         let a = Q.((ci1-ci2) / (ch1-ch2)) in
         let b = Q.(ci2 - a*ch2) in
         Rhs.canonicalize (Some (Z.(a.num*b.den),xh),Z.(b.num*a.den) ,Z.(a.den*b.den) ) in
-      let iterate map l = 
+      let iterate map l =
         match l with
         | (_, _, _, rhs                  , rhs'                 ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_)      -> EConj.set_rhs acc x rh) map l
         | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_)       )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_)         -> EConj.set_rhs acc i (varentry   Q.(make (fst@@Option.get monom) di)   Q.(make oi di)   Q.(make ch dh)   Q.(make oh dh)   h)) map t
@@ -630,8 +630,8 @@ struct
 
   let assign_exp ask t var exp no_ov =
     let res = assign_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s"
-        (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
+    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s"
+        (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res);
     res
 
   let assign_var (t: VarManagement.t) v v' =
@@ -640,7 +640,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ;
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
     res
 
   (** Parallel assignment of variables.
@@ -693,7 +693,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 9627b4762a..1e0a223571 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -136,7 +136,7 @@ struct
             let expr =
               (** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively
                   this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they
-                  might be able to be represented by means of 2 var equalities 
+                  might be able to be represented by means of 2 var equalities
 
                   This simplification happens during a time, when there are temporary variables a#in and a#out part of the expression,
                   but are not represented in the ctx, thus queries may result in top for these variables. Wrapping this in speculative
@@ -279,7 +279,7 @@ struct
           expr := BinOp(MinusA,!expr,prod,longlong)
         else
           expr := BinOp(PlusA,!expr,prod,longlong)
-      | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s"  (Var.to_string v); raise Unsupported_Linexpr1
+      | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1
     in
     Linexpr1.iter append_summand linexpr1;
     !expr

From b735727192db12f77c2778fd2d21d2d1c431e3ce Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 17 Jul 2024 11:24:22 +0300
Subject: [PATCH 30/34] Add Printable functions to GobApron.Scalar

---
 src/cdomains/apron/gobApron.apron.ml        | 13 +++++++++++++
 src/cdomains/apron/sharedFunctions.apron.ml |  4 ++--
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index fca28ff8f0..80d32f1821 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -1,6 +1,19 @@
 open Batteries
 include Apron
 
+module Scalar =
+struct
+  include Scalar
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+end
+
 module Coeff =
 struct
   include Coeff
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 1e0a223571..dc918be571 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -36,7 +36,7 @@ let int_of_scalar ?round (scalar: Scalar.t) =
       in
       Z_mlgmpidl.z_of_mpzf z
     | _ ->
-      failwith ("int_of_scalar: unsupported: " ^ Scalar.to_string scalar)
+      failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
 
 module type ConvertArg =
@@ -263,7 +263,7 @@ struct
                else
                  Const (CInt(i,ILongLong,None)), false
            else
-             (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %s" (Scalar.to_string c); raise Unsupported_Linexpr1)
+             (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
          | None -> raise Unsupported_Linexpr1)
       | _ -> raise Unsupported_Linexpr1
     in

From 8f0ebc506662946192a96faf75e97af9fdeabf70 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 17 Jul 2024 11:24:43 +0300
Subject: [PATCH 31/34] Use GobZ.pretty in lin2var tracing

---
 src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index c13aca60ea..65775d9188 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -361,7 +361,7 @@ struct
     else
       match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with
       | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in
-        (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string res) (IntOps.BigIntOps.to_string res);
+        (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res;
          Some res, Some res)
       | _ -> None, None
 

From 06ea5e050df7d03692912bbfc3022a068cf411f4 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 17 Jul 2024 13:24:46 +0200
Subject: [PATCH 32/34] Rm resolved TODO

---
 src/cdomains/apron/sharedFunctions.apron.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index a9406d48e9..8121635e89 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -275,7 +275,6 @@ struct
     let append_summand (c:Coeff.union_5) v =
       match V.to_cil_varinfo v with
       | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-        (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *)
         let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
         let coeff, flip = coeff_to_const true c in
         let prod = BinOp(Mult, coeff, var, longlong) in
@@ -291,7 +290,7 @@ struct
 
 
   let lcm_den linexpr1 =
-    let exception UnsupportedScalar 
+    let exception UnsupportedScalar
     in
     let frac_of_scalar scalar =
       if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)

From 62f1e2e0de72df4b09ffcd7d34a86c1616c740af Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 26 Jun 2024 17:43:07 +0300
Subject: [PATCH 33/34] Try to print selenium logs for Gobview test

---
 scripts/test-gobview.py | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py
index f5961108d7..10808a9b62 100644
--- a/scripts/test-gobview.py
+++ b/scripts/test-gobview.py
@@ -6,6 +6,7 @@
 from webdriver_manager.chrome import ChromeDriverManager
 from selenium.webdriver.common.by import By
 from selenium.webdriver.chrome.options import Options
+from selenium.webdriver.common.desired_capabilities import DesiredCapabilities
 from threading import Thread
 import subprocess
 
@@ -17,6 +18,11 @@
 # cleanup
 def cleanup(browser, thread):
   print("cleanup")
+
+  # print messages
+  for entry in browser.get_log('browser'):
+    print(entry)
+
   browser.close()
   p.kill()
   thread.join()
@@ -35,6 +41,8 @@ def serve():
 print("starting installation of browser\n")
 options = Options()
 options.add_argument('headless')
+# options.set_capability("loggingPrefs", { 'browser':'ALL' })
+options.set_capability("goog:loggingPrefs", { 'browser':'ALL' })
 browser = webdriver.Chrome(service=Service(ChromeDriverManager().install()),options=options)
 print("finished webdriver installation \n")
 browser.maximize_window()

From 23643df9f573ab88296247fe17a07dc3205db249 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 24 Jul 2024 10:46:11 +0300
Subject: [PATCH 34/34] Add js_of_ocaml upper bound for Gobview

---
 gobview | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gobview b/gobview
index 4069f32f82..03b0682f97 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 4069f32f82efdefb43c970fb77ca29671a4b6972
+Subproject commit 03b0682f973eab0d26cf8aea74c63a9e869c9716