From 0193efad541bb0ba9d3ee79b3b8cf1dabd9aff05 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 10 Sep 2023 12:59:02 +0200
Subject: [PATCH 01/42] handle `bitand` in congruences in restricted cases

---
 src/cdomains/intDomain.ml | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 5417598360..c78e66e2bf 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -514,7 +514,7 @@ module Size = struct (* size in bits as int, range as int64 *)
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
     if t = IBool then
-      (* C11 6.3.1.2 Boolean type *) 
+      (* C11 6.3.1.2 Boolean type *)
       if Z.equal x Z.zero then Z.zero else Z.one
     else
       let a,b = range t in
@@ -1978,7 +1978,7 @@ struct
   let top_of ik = `Excluded (S.empty (), size ik)
   let cast_to ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
-      let r' = size ik in 
+      let r' = size ik in
         if R.leq r r' then (* upcast -> no change *)
           `Excluded (s, r)
         else if ik = IBool then (* downcast to bool *)
@@ -1986,7 +1986,7 @@ struct
             `Definite (BI.one)
           else
             `Excluded (S.empty(), r')
-        else 
+        else
           (* downcast: may overflow *)
           (* let s' = S.map (BigInt.cast_to ik) s in *)
           (* We want to filter out all i in s' where (t)x with x in r could be i. *)
@@ -3134,7 +3134,7 @@ struct
 
   (** The implementation of the bit operations could be improved based on the master’s thesis
       'Abstract Interpretation and Abstract Domains' written by Stefan Bygde.
-      see: https://www.dsi.unive.it/~avp/domains.pdf *)
+      see: http://www.es.mdh.se/pdf_publications/948.pdf *)
   let bit2 f ik x y = match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
@@ -3144,7 +3144,19 @@ struct
 
   let bitor ik x y = bit2 Ints_t.bitor ik x y
 
-  let bitand ik x y = bit2 Ints_t.bitand ik x y
+  let bitand ik x y =  match x, y with
+    | None, None -> None
+    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
+    | Some (c, m), Some (c', m') ->
+      if (m =: Ints_t.zero && m' =: Ints_t.zero) then
+        (* both arguments constant *)
+        Some (Ints_t.bitand c c', Ints_t.zero)
+      else if m' =: Ints_t.zero && c' =: Ints_t.one && Ints_t.rem m (Ints_t.of_int 2) =: Ints_t.zero then
+        (* x & 1  and  x == c (mod 2*z) *)
+        (* Value is equal to LSB of c *)
+        Some (Ints_t.bitand c c', Ints_t.zero)
+      else
+        top ()
 
   let bitxor ik x y = bit2 Ints_t.bitxor ik x y
 

From 4d18300af5f6ae1b04bdbf29b29775af07fbc96c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 10 Sep 2023 13:53:37 +0200
Subject: [PATCH 02/42] Handle `bitand` in intervals and def_exc; Add test

---
 src/analyses/baseInvariant.ml              | 26 ++++++++++----
 src/cdomains/intDomain.ml                  | 36 +++++++++++++++++--
 tests/regression/37-congruence/13-bitand.c | 40 ++++++++++++++++++++++
 3 files changed, 93 insertions(+), 9 deletions(-)
 create mode 100644 tests/regression/37-congruence/13-bitand.c

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 096d50b89b..70c6ed9101 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -410,6 +410,18 @@ struct
           meet_bin c c
         else
           a, b
+      | BAnd as op ->
+        (* we only attempt to refine a here *)
+        let a =
+          match ID.to_int b with
+          | Some x when BI.equal x BI.one ->
+            (match ID.to_bool c with
+             | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
+             | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
+             | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a\n" d_binop op ID.pretty c; a)
+          | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a\n" d_binop op ID.pretty b ID.pretty c; a
+        in
+        a, b
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op;
         a, b
@@ -545,8 +557,8 @@ struct
     in
     let eval e st = eval_rv a gs st e in
     let eval_bool e st = match eval e st with Int i -> ID.to_bool i | _ -> None in
-    let unroll_fk_of_exp e = 
-      match unrollType (Cilfacade.typeOf e) with 
+    let unroll_fk_of_exp e =
+      match unrollType (Cilfacade.typeOf e) with
       | TFloat (fk, _) -> fk
       | _ -> failwith "value which was expected to be a float is of different type?!"
     in
@@ -700,8 +712,8 @@ struct
               begin match t with
                 | TInt (ik, _) ->
                   begin match x with
-                    | ((Var v), offs) -> 
-                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); 
+                    | ((Var v), offs) ->
+                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       let tv_opt = ID.to_bool c in
                       begin match tv_opt with
                         | Some tv ->
@@ -735,12 +747,12 @@ struct
               begin match t with
                 | TFloat (fk, _) ->
                   begin match x with
-                    | ((Var v), offs) -> 
-                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); 
+                    | ((Var v), offs) ->
+                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
                         | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
                         | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
-                        | `Lifted (Fabs (ret_fk, xFloat)) -> 
+                        | `Lifted (Fabs (ret_fk, xFloat)) ->
                           let inv = FD.inv_fabs (FD.cast_to ret_fk c) in
                           if FD.is_bot inv then
                             raise Analyses.Deadcode
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index c78e66e2bf..312f5d7540 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -826,7 +826,18 @@ struct
       | _              -> (top_of ik,{underflow=true; overflow=true})
 
   let bitxor = bit (fun _ik -> Ints_t.bitxor)
-  let bitand = bit (fun _ik -> Ints_t.bitand)
+
+  let bitand ik i1 i2 =
+    match is_bot i1, is_bot i2 with
+    | true, true -> bot_of ik
+    | true, _
+    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
+    | _ ->
+      match to_int i1, to_int i2 with
+      | Some x, Some y -> (try of_int ik (Ints_t.bitand x y) |> fst with Division_by_zero -> top_of ik)
+      | _, Some y  when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
+      | _ -> top_of ik
+
   let bitor  = bit (fun _ik -> Ints_t.bitor)
 
   let bit1 f ik i1 =
@@ -2282,7 +2293,28 @@ struct
   let ge ik x y = le ik y x
 
   let bitnot = lift1 BigInt.bitnot
-  let bitand = lift2 BigInt.bitand
+
+  let bitand ik x y = norm ik (match x,y with
+      (* We don't bother with exclusion sets: *)
+      | `Excluded _, `Definite i ->
+        (* Except in two special cases *)
+        if BigInt.equal i BigInt.zero then
+          `Definite BigInt.zero
+        else if BigInt.equal i BigInt.one then
+          of_interval IBool (BigInt.zero, BigInt.one)
+        else
+          top ()
+      | `Definite _, `Excluded _
+      | `Excluded _, `Excluded _ -> top ()
+      (* The good case: *)
+      | `Definite x, `Definite y ->
+        (try `Definite (BigInt.bitand x y) with | Division_by_zero -> top ())
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
+
+
   let bitor  = lift2 BigInt.bitor
   let bitxor = lift2 BigInt.bitxor
 
diff --git a/tests/regression/37-congruence/13-bitand.c b/tests/regression/37-congruence/13-bitand.c
new file mode 100644
index 0000000000..c785e722c1
--- /dev/null
+++ b/tests/regression/37-congruence/13-bitand.c
@@ -0,0 +1,40 @@
+// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
+#include <goblint.h>
+
+int main()
+{
+	// Assuming modulo expression
+
+	long x;
+	__goblint_assume(x % 2 == 1);
+	__goblint_check(x % 2 == 1);
+	__goblint_check(x & 1);
+
+	long y;
+	__goblint_assume(y % 2 == 0);
+	__goblint_check(y % 2 == 0);
+	__goblint_check(y & 1); //FAIL
+
+	long z;
+	__goblint_check(z & 1); //UNKNOWN!
+	__goblint_assume(z % 8 == 1);
+	__goblint_check(z & 1);
+
+	long xz;
+	__goblint_assume(xz % 3 == 1);
+	__goblint_check(xz & 1); //UNKNOWN!
+	__goblint_assume(xz % 6 == 1);
+	__goblint_check(xz & 1);
+
+	// Assuming bitwise expression
+
+	long a;
+	__goblint_assume(a & 1);
+	__goblint_check(a % 2 == 1);
+	__goblint_check(a & 1);
+
+	int b;
+	__goblint_assume(b & 1);
+	__goblint_check(b % 2 == 1);
+	__goblint_check(b & 1);
+}

From e40255bdaca9bebe56ccde7f77ded60c25af9023 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 11 Sep 2023 12:52:13 +0200
Subject: [PATCH 03/42] Add special case for &0 in the interval domain

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

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 312f5d7540..f1ed546e95 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -835,7 +835,8 @@ struct
     | _ ->
       match to_int i1, to_int i2 with
       | Some x, Some y -> (try of_int ik (Ints_t.bitand x y) |> fst with Division_by_zero -> top_of ik)
-      | _, Some y  when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
+      | _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
+      | _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
       | _ -> top_of ik
 
   let bitor  = bit (fun _ik -> Ints_t.bitor)

From f643bb5ad0ae3c7e4f012d91be88e1557de7bd1a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 13:37:25 +0300
Subject: [PATCH 04/42] Add external benchmarking guide

---
 docs/user-guide/benchmarking.md | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/docs/user-guide/benchmarking.md b/docs/user-guide/benchmarking.md
index 44811b61a5..5417375bdb 100644
--- a/docs/user-guide/benchmarking.md
+++ b/docs/user-guide/benchmarking.md
@@ -1,6 +1,31 @@
 # Benchmarking
+The following best practices should be followed when benchmarking Goblint.
+This is to ensure valid, reproducible and representative benchmarking results.
 
-To achieve reproducible builds and the best performance for benchmarking, it is recommended to compile Goblint using the `release` option:
+# External benchmarking
+External users should choose the version of Goblint to evaluate or benchmark as follows:
+
+1. Use the newest version release.
+
+    The version from git `master` branch or any other intermediate git commit come without any guarantees.
+    They are bleeding-edge and haven't gone through validation like the version releases.
+
+    SV-COMP releases are highly preferable since they've gone through rigorous validation in SV-COMP.
+
+2. Download the corresponding version from a Zenodo artifact or by checking out the respective git tag. **Do not install directly from opam repository!**
+
+    Goblint pins optimized versions of some dependencies which cannot be done on the opam repository releases.
+    Thus, using the latter would yield unrepresentative results.
+
+    Zenodo artifacts come with DOIs, which make them ideal for citation.
+
+3. Use OCaml 4.14. **Do not use OCaml 5!**
+
+    OCaml 5 has significant performance regressions, which yield unrepresentative benchmarking results.
+    Goblint's `make setup` installs the correct OCaml version into a new opam switch.
+
+# Release build
+To achieve the best performance for benchmarking, Goblint should be compiled using the `release` option:
 
 ```sh
 make release

From a3eaf9aece32da7a67d65dc17bffa57dbc9b8530 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 13:39:42 +0300
Subject: [PATCH 05/42] Refer to benchmarking guide in README

---
 README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/README.md b/README.md
index b03b7bbe36..4d97baa842 100644
--- a/README.md
+++ b/README.md
@@ -13,6 +13,7 @@ Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/e
 
 ## Installing
 Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
+For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/).
 
 ### Linux
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).

From cd45df53d63174ad77f05d93d34472f4cdbd639a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 14:02:11 +0300
Subject: [PATCH 06/42] Add opam post-message about OCaml 5 benchmarking

---
 goblint.opam          | 3 +++
 goblint.opam.locked   | 3 +++
 goblint.opam.template | 3 +++
 3 files changed, 9 insertions(+)

diff --git a/goblint.opam b/goblint.opam
index a20df919d0..59f8a59c09 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -81,3 +81,6 @@ pin-depends: [
   # TODO: add back after release, only pinned for CI stability
   [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
 ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
+]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index acb49a7b14..fe5bb65a00 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -140,3 +140,6 @@ pin-depends: [
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
   ]
 ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
+]
diff --git a/goblint.opam.template b/goblint.opam.template
index b7f5a7abff..5c13293196 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -8,3 +8,6 @@ pin-depends: [
   # TODO: add back after release, only pinned for CI stability
   [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
 ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
+]

From ee31392babcb1107763f5b5658215716c7d90dc3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Aug 2023 17:49:48 +0300
Subject: [PATCH 07/42] Use opam 2.0 compatible switch create (closes #1133)

---
 make.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/make.sh b/make.sh
index 788289c5ed..af1411a8d3 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 ocaml-variants.4.14.0+options ocaml-option-flambda --locked
+  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda --locked
 }
 
 rule() {

From b25cb45cca2d755d26c86dfe9529ce15b761a161 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 14:23:02 +0300
Subject: [PATCH 08/42] Use OCaml 5.0 compatible Apron

---
 goblint.opam          |  2 --
 goblint.opam.locked   | 12 ++++--------
 goblint.opam.template |  2 --
 3 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index 59f8a59c09..794b43e770 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -78,8 +78,6 @@ pin-depends: [
   [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
   # 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" ]
-  # TODO: add back after release, only pinned for CI stability
-  [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index fe5bb65a00..5f81506183 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -21,7 +21,7 @@ doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.13"}
+  "apron" {= "v0.9.14~beta.2"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
@@ -56,22 +56,22 @@ depends: [
   "dune-private-libs" {= "3.6.1"}
   "dune-site" {= "3.6.1"}
   "dyn" {= "3.6.1"}
+  "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
   "goblint-cil" {= "2.0.1"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "0.12.1"}
   "jsonrpc" {= "1.15.0~5.0preview1"}
-  "fileutils" {= "0.6.4"}
   "logs" {= "0.7.0"}
-  "mlgmpidl" {= "1.2.14"}
+  "mlgmpidl" {= "1.2.15"}
   "num" {= "1.4"}
   "ocaml" {= "4.14.0"}
-  "ocaml-variants" {= "4.14.0+options"}
   "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}
@@ -131,10 +131,6 @@ pin-depends: [
     "goblint-cil.2.0.1"
     "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e"
   ]
-  [
-    "apron.v0.9.13"
-    "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"
-  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
diff --git a/goblint.opam.template b/goblint.opam.template
index 5c13293196..ff1364fc20 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -5,8 +5,6 @@ pin-depends: [
   [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
   # 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" ]
-  # TODO: add back after release, only pinned for CI stability
-  [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}

From 13062dfc37b5b1108bf44081c0c0b8363ce81083 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 14:24:26 +0300
Subject: [PATCH 09/42] Add OCaml 5.0 to unlocked workflow

---
 .github/workflows/unlocked.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 15cd9138d8..65d85f0b3d 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -18,6 +18,7 @@ jobs:
           - ubuntu-latest
           - macos-latest
         ocaml-compiler:
+          - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
           - 4.14.x
           - 4.13.x

From 94db94deb38ffa5b880214d36c17defbf53683df Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 14:32:45 +0300
Subject: [PATCH 10/42] Update Gobview to OCaml 5 compatible

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

diff --git a/gobview b/gobview
index c3dcfaba97..70f76a1692 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit c3dcfaba97a1df72f027e5dad317e2c201ce5e4b
+Subproject commit 70f76a16927b14fca0ccfd3ab032076381bdc834

From bff915968251f99b5ba14ac4dfa1021f0b2c371b Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 12 Sep 2023 16:03:00 +0200
Subject: [PATCH 11/42] Congruences: Make % sound by restricting cases where we
 return a constant

---
 src/cdomains/intDomain.ml                         |  4 ++--
 tests/regression/37-congruence/06-refinements.c   |  5 +++--
 tests/regression/37-congruence/07-refinements-o.c |  5 +++--
 .../regression/37-congruence/11-overflow-signed.c |  6 +++---
 tests/regression/37-congruence/13-bitand.c        | 12 +++++++++---
 tests/regression/37-congruence/14-negative.c      | 15 +++++++++++++++
 6 files changed, 35 insertions(+), 12 deletions(-)
 create mode 100644 tests/regression/37-congruence/14-negative.c

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index f1ed546e95..748df62300 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -3199,8 +3199,8 @@ struct
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some(c2, m2) ->
       if m2 =: Ints_t.zero then
-        if (c2 |: m1) then
-          Some(c1 %: c2,Ints_t.zero)
+        if (c2 |: m1) && (c1 %: c2 =: Ints_t.zero || m1 =: Ints_t.zero || not (Cil.isSigned ik)) then
+          Some(c1 %: c2, Ints_t.zero)
         else
           normalize ik (Some(c1, (Ints_t.gcd m1 c2)))
       else
diff --git a/tests/regression/37-congruence/06-refinements.c b/tests/regression/37-congruence/06-refinements.c
index c0b7b0564c..38bf9458cc 100644
--- a/tests/regression/37-congruence/06-refinements.c
+++ b/tests/regression/37-congruence/06-refinements.c
@@ -5,14 +5,15 @@ int main() {
     int top;
     int i = 0;
     if(top % 17 == 3) {
-        __goblint_check(top%17 ==3);
+        __goblint_check(top%17 ==3); //TODO (Refine top to be positive above, and reuse information in %)
         if(top %17 != 3) {
             i = 12;
         } else {
 
         }
     }
-    __goblint_check(i ==0);
+    __goblint_check(i ==0); // TODO
+    i = 0;
 
     if(top % 17 == 0) {
         __goblint_check(top%17 == 0);
diff --git a/tests/regression/37-congruence/07-refinements-o.c b/tests/regression/37-congruence/07-refinements-o.c
index 44f21b7c8c..49148d6683 100644
--- a/tests/regression/37-congruence/07-refinements-o.c
+++ b/tests/regression/37-congruence/07-refinements-o.c
@@ -32,15 +32,16 @@ int main() {
     int top;
     int i = 0;
     if(top % 17 == 3) {
-        __goblint_check(top%17 ==3);
+        __goblint_check(top%17 ==3); //TODO (Refine top to be positive above, and reuse information in %)
         if(top %17 != 3) {
             i = 12;
         } else {
 
         }
     }
-    __goblint_check(i ==0);
+    __goblint_check(i ==0); //TODO
 
+    i = 0;
     if(top % 17 == 0) {
         __goblint_check(top%17 == 0);
         if(top %17 != 0) {
diff --git a/tests/regression/37-congruence/11-overflow-signed.c b/tests/regression/37-congruence/11-overflow-signed.c
index 29599fe246..031d88ce45 100644
--- a/tests/regression/37-congruence/11-overflow-signed.c
+++ b/tests/regression/37-congruence/11-overflow-signed.c
@@ -12,8 +12,8 @@ int basic(){
 	{
 		if (b % two_pow_16 == 5)
 		{
-			__goblint_check(a % two_pow_16 == 3);
-			__goblint_check(b % two_pow_16 == 5);
+			__goblint_check(a % two_pow_16 == 3); //TODO (Refine a to be positive above, and reuse information in %)
+			__goblint_check(b % two_pow_16 == 5); //TODO (Refine a to be positive above, and reuse information in %)
 
 			unsigned int e = a * b;
 			__goblint_check(e % two_pow_16 == 15); // UNKNOWN!
@@ -35,7 +35,7 @@ int special(){
 
 	if (a % two_pow_18 == two_pow_17)
 	{
-		__goblint_check(a % two_pow_18 == two_pow_17);
+		__goblint_check(a % two_pow_18 == two_pow_17); //TODO (Refine a to be positive above, and reuse information in %)
 
 		unsigned int e = a * a;
 		__goblint_check(e == 0); //UNKNOWN!
diff --git a/tests/regression/37-congruence/13-bitand.c b/tests/regression/37-congruence/13-bitand.c
index c785e722c1..500fb9d1cc 100644
--- a/tests/regression/37-congruence/13-bitand.c
+++ b/tests/regression/37-congruence/13-bitand.c
@@ -5,11 +5,16 @@ int main()
 {
 	// Assuming modulo expression
 
-	long x;
+	unsigned long x;
 	__goblint_assume(x % 2 == 1);
 	__goblint_check(x % 2 == 1);
 	__goblint_check(x & 1);
 
+	long xx;
+	__goblint_assume(xx % 2 == 1);
+	__goblint_check(xx % 2 == 1); //TODO (Refine xx to be positive above, and reuse information in %)
+	__goblint_check(xx & 1);
+
 	long y;
 	__goblint_assume(y % 2 == 0);
 	__goblint_check(y % 2 == 0);
@@ -27,14 +32,15 @@ int main()
 	__goblint_check(xz & 1);
 
 	// Assuming bitwise expression
+	// Does NOT actually lead to modulo information, as negative values may also have their last bit set!
 
 	long a;
 	__goblint_assume(a & 1);
-	__goblint_check(a % 2 == 1);
+	__goblint_check(a % 2 == 1); //UNKNOWN!
 	__goblint_check(a & 1);
 
 	int b;
 	__goblint_assume(b & 1);
-	__goblint_check(b % 2 == 1);
+	__goblint_check(b % 2 == 1); //UNKNOWN!
 	__goblint_check(b & 1);
 }
diff --git a/tests/regression/37-congruence/14-negative.c b/tests/regression/37-congruence/14-negative.c
new file mode 100644
index 0000000000..eae8307ab1
--- /dev/null
+++ b/tests/regression/37-congruence/14-negative.c
@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
+#include <goblint.h>
+
+int main()
+{
+	int top;
+
+	int c = -5;
+	if (top)
+	{
+		c = -7;
+	}
+	__goblint_check(c % 2 == 1); //UNKNOWN! (Does not hold at runtime)
+	__goblint_check(c % 2 == -1); //TODO (Track information that c is negative)
+}

From c6e43c552ec54324e793954aa616b0b21b1d717f Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 12 Sep 2023 20:07:09 +0000
Subject: [PATCH 12/42] Bump docker/build-push-action from 4 to 5

Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 4 to 5.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v4...v5)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
---
 .github/workflows/docker.yml   | 4 ++--
 .github/workflows/unlocked.yml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 1ef104db29..b0f7b30f01 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: true
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 15cd9138d8..f5a5ef0138 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -215,7 +215,7 @@ jobs:
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           target: dev

From 72550593ba3b4157a0ed4ea6bde1f1974e31c1c6 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 12 Sep 2023 20:07:12 +0000
Subject: [PATCH 13/42] Bump docker/metadata-action from 4 to 5

Bumps [docker/metadata-action](https://github.com/docker/metadata-action) from 4 to 5.
- [Release notes](https://github.com/docker/metadata-action/releases)
- [Upgrade guide](https://github.com/docker/metadata-action/blob/master/UPGRADE.md)
- [Commits](https://github.com/docker/metadata-action/compare/v4...v5)

---
updated-dependencies:
- dependency-name: docker/metadata-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
---
 .github/workflows/docker.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 1ef104db29..40647f1335 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -49,7 +49,7 @@ jobs:
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
-        uses: docker/metadata-action@v4
+        uses: docker/metadata-action@v5
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |

From 25ce122603ca04eea4323b2448bb290cb0bc2b93 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 12 Sep 2023 20:07:16 +0000
Subject: [PATCH 14/42] Bump docker/setup-buildx-action from 2 to 3

Bumps [docker/setup-buildx-action](https://github.com/docker/setup-buildx-action) from 2 to 3.
- [Release notes](https://github.com/docker/setup-buildx-action/releases)
- [Commits](https://github.com/docker/setup-buildx-action/compare/v2...v3)

---
updated-dependencies:
- dependency-name: docker/setup-buildx-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
---
 .github/workflows/docker.yml   | 2 +-
 .github/workflows/unlocked.yml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 1ef104db29..716ad314bf 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -38,7 +38,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
         uses: docker/login-action@v2
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 15cd9138d8..15179fda03 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -211,7 +211,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Build dev Docker image
         id: build

From 02c839f198c48b3256aa815ade4590c3a159bf0c Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Tue, 12 Sep 2023 20:07:20 +0000
Subject: [PATCH 15/42] Bump docker/login-action from 2 to 3

Bumps [docker/login-action](https://github.com/docker/login-action) from 2 to 3.
- [Release notes](https://github.com/docker/login-action/releases)
- [Commits](https://github.com/docker/login-action/compare/v2...v3)

---
updated-dependencies:
- dependency-name: docker/login-action
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
---
 .github/workflows/docker.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 1ef104db29..410aa05ea1 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -41,7 +41,7 @@ jobs:
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}

From bef3c54e0f6c5c13aca320774107cc626cb79368 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 10:43:00 +0300
Subject: [PATCH 16/42] Replace goblint-cil pin with published 2.0.2

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

diff --git a/dune-project b/dune-project
index b8b8481c97..c5dc943c5d 100644
--- a/dune-project
+++ b/dune-project
@@ -24,7 +24,7 @@
   (synopsis "Static analysis framework for C")
   (depends
     (ocaml (>= 4.10))
-    (goblint-cil (>= 2.0.1)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
+    (goblint-cil (>= 2.0.2)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.4.0))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
diff --git a/goblint.opam b/goblint.opam
index 59f8a59c09..3b1afdfff8 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -21,7 +21,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.6"}
   "ocaml" {>= "4.10"}
-  "goblint-cil" {>= "2.0.1"}
+  "goblint-cil" {>= "2.0.2"}
   "batteries" {>= "3.4.0"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
@@ -75,7 +75,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
+  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # 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" ]
   # TODO: add back after release, only pinned for CI stability
diff --git a/goblint.opam.locked b/goblint.opam.locked
index fe5bb65a00..d0323713ad 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -58,7 +58,7 @@ depends: [
   "dyn" {= "3.6.1"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.1"}
+  "goblint-cil" {= "2.0.2"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "0.12.1"}
   "jsonrpc" {= "1.15.0~5.0preview1"}
@@ -127,10 +127,6 @@ conflicts: [
 ]
 # TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
-  [
-    "goblint-cil.2.0.1"
-    "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e"
-  ]
   [
     "apron.v0.9.13"
     "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"
diff --git a/goblint.opam.template b/goblint.opam.template
index 5c13293196..eb795f29d2 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -2,7 +2,8 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
+  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # 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" ]
   # TODO: add back after release, only pinned for CI stability
diff --git a/gobview b/gobview
index c3dcfaba97..b373d06174 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit c3dcfaba97a1df72f027e5dad317e2c201ce5e4b
+Subproject commit b373d06174667537b671f3122daf4ebd4b195aea

From 8440ff01c6f63e9480b578e79bb7dc28893ed5e1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 11:08:32 +0300
Subject: [PATCH 17/42] Update releasing documentation about Zenodo webhook

---
 docs/developer-guide/releasing.md | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
index f6bfbb459e..69ffcb2461 100644
--- a/docs/developer-guide/releasing.md
+++ b/docs/developer-guide/releasing.md
@@ -45,13 +45,20 @@
     10. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
     11. Exit Docker container.
 
-12. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
+12. Temporarily enable Zenodo GitHub webhook.
+
+    This is because we only want numbered version releases to automatically add a new version to our Zenodo artifact.
+    Other tags (like SV-COMP or paper artifacts) have manually created Zenodo artifacts anyway and thus shouldn't add new versions to the main Zenodo artifact.
+
+13. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
 
     Explicitly specify `distrib` because we don't want to publish OCaml API docs.
     Environment variable workaround for the package having a Read the Docs `doc` URL (see <https://github.com/ocamllabs/dune-release/issues/154>).
 
-13. Create an opam package: `dune-release opam pkg`.
-14. Submit the opam package to opam-repository: `dune-release opam submit`.
+14. Re-disable Zenodo GitHub webhook.
+
+15. Create an opam package: `dune-release opam pkg`.
+16. Submit the opam package to opam-repository: `dune-release opam submit`.
 
 
 ## SV-COMP
@@ -104,15 +111,9 @@
 ### After all preruns
 
 1. Push git tag from last prerun: `git push origin svcompXY`.
-2. Temporarily disable Zenodo webhook.
-
-    This is because we don't want a new out-of-place version of Goblint in our Zenodo artifact.
-    A separate Zenodo artifact for the SV-COMP version can be created later if tool paper is submitted.
-
-3. Create GitHub release from the git tag and attach latest submitted archive as a download.
-4. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
+2. Create GitHub release from the git tag and attach latest submitted archive as a download.
+3. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
 
     This is because the usual `docker` workflow only handles semver releases.
 
-5. Re-enable Zenodo webhook.
-6. Release new semver version on opam. See above.
+4. Release new semver version on opam. See above.

From 336c5ffaa050cdd8e9760b0fad7565df5351892f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 11:26:57 +0300
Subject: [PATCH 18/42] Finalize v2.2.0 CHANGELOG

---
 CHANGELOG.md | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a126514852..045e06815a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,6 @@
 ## v2.2.0
-* TODO OCaml 5 (#1003, #1137).
-* TODO Library #1138
-* TODO refactor race #1136
-
 * Add `setjmp`/`longjmp` analysis (#887, #970, #1015, #1019).
-* Refactor race analysis to lazy distribution (#1084, #1089, #1016).
+* Refactor race analysis to lazy distribution (#1084, #1089, #1136, #1016).
 * Add thread-unsafe library function call analysis (#723, #1082).
 * Add mutex type analysis and mutex API analysis (#800, #839, #1073).
 * Add interval set domain and string literals domain (#901, #966, #994, #1048).
@@ -19,8 +15,8 @@
 * Fix many incremental analysis issues (#627, #836, #835, #841, #932, #678, #942, #949, #950, #957, #955, #954, #960, #959, #1004, #558, #1010, #1091).
 * Fix server mode for abstract debugging (#983, #990, #997, #1000, #1001, #1013, #1018, #1017, #1026, #1027).
 * Add documentation for configuration JSON schema and OCaml API (#999, #1054, #1055, #1053).
-* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135).
-* Add OCaml 5.0 support (#945).
+* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135, #1138).
+* Add OCaml 5.0 support (#1003, #945, #1162).
 
 ## v2.1.0
 Functionally equivalent to Goblint in SV-COMP 2023.

From b46aeda9eaecd3ec42ec14c977d1550faad0de23 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 11:29:16 +0300
Subject: [PATCH 19/42] Disable pins for v2.2.0 release

---
 goblint.opam          | 6 +++---
 goblint.opam.locked   | 7 -------
 goblint.opam.template | 6 +++---
 3 files changed, 6 insertions(+), 13 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index e42f4f7f47..efdd0aaa00 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -74,12 +74,12 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
+# pin-depends: [
   # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
   # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # 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" ]
-]
+  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+# ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index b97faad221..bb59c41dd1 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -125,13 +125,6 @@ available: os-distribution != "alpine" & arch != "arm64"
 conflicts: [
   "result" {< "1.5"}
 ]
-# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
-pin-depends: [
-  [
-    "ppx_deriving.5.2.1"
-    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
-  ]
-]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.template b/goblint.opam.template
index 59160bf171..6259c4d498 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,12 +1,12 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
+# pin-depends: [
   # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
   # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # 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" ]
-]
+  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+# ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

From 246c999ad775c7f4bb8db7989fc975ab5d774444 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 14:45:29 +0300
Subject: [PATCH 20/42] Bump batteries lower bound to 3.5.0

Required for Hashtbl.exists.
---
 dune-project | 2 +-
 goblint.opam | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/dune-project b/dune-project
index c5dc943c5d..4a9cd8e3c1 100644
--- a/dune-project
+++ b/dune-project
@@ -25,7 +25,7 @@
   (depends
     (ocaml (>= 4.10))
     (goblint-cil (>= 2.0.2)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
-    (batteries (>= 3.4.0))
+    (batteries (>= 3.5.0))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
diff --git a/goblint.opam b/goblint.opam
index efdd0aaa00..661222805b 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -22,7 +22,7 @@ depends: [
   "dune" {>= "3.6"}
   "ocaml" {>= "4.10"}
   "goblint-cil" {>= "2.0.2"}
-  "batteries" {>= "3.4.0"}
+  "batteries" {>= "3.5.0"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}

From 1a731fd3eb9bed59843d0e5a9e96694d6592a1a5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 15:10:54 +0300
Subject: [PATCH 21/42] Fix deprecated tail syntax in
 70-transform/02-deadcode.t

---
 tests/regression/70-transform/02-deadcode.t | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/70-transform/02-deadcode.t b/tests/regression/70-transform/02-deadcode.t
index ed3cd80e17..8bc4f9bf13 100644
--- a/tests/regression/70-transform/02-deadcode.t
+++ b/tests/regression/70-transform/02-deadcode.t
@@ -210,7 +210,7 @@
 
 Transformation still works with 'exp.mincfg', but can not find all dead code; test against the diff.
 Macintosh's diff(1) adds whitespace after the function names, strip with sed.
-  $ diff -p -U0 "$(./transform.sh --file $args 02-deadcode.c)" "$(./transform.sh --file $args --enable exp.mincfg 02-deadcode.c)" | sed 's/[[:blank:]]*$//' | tail +3
+  $ diff -p -U0 "$(./transform.sh --file $args 02-deadcode.c)" "$(./transform.sh --file $args --enable exp.mincfg 02-deadcode.c)" | sed 's/[[:blank:]]*$//' | tail -n +3
   @@ -13,0 +14,3 @@ int basic1(int n )
   +  if (n < 0) {
   +    return (0);

From 833d90d41b5d14934edbf283cb90fdafbf382798 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 15:16:01 +0300
Subject: [PATCH 22/42] Remove -p in 70-transform/02-deadcode.t due to OSX

On opam-repository CI, OSX has different -p output.
---
 tests/regression/70-transform/02-deadcode.t | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/regression/70-transform/02-deadcode.t b/tests/regression/70-transform/02-deadcode.t
index 8bc4f9bf13..03a46b891e 100644
--- a/tests/regression/70-transform/02-deadcode.t
+++ b/tests/regression/70-transform/02-deadcode.t
@@ -210,15 +210,15 @@
 
 Transformation still works with 'exp.mincfg', but can not find all dead code; test against the diff.
 Macintosh's diff(1) adds whitespace after the function names, strip with sed.
-  $ diff -p -U0 "$(./transform.sh --file $args 02-deadcode.c)" "$(./transform.sh --file $args --enable exp.mincfg 02-deadcode.c)" | sed 's/[[:blank:]]*$//' | tail -n +3
-  @@ -13,0 +14,3 @@ int basic1(int n )
+  $ diff -U0 "$(./transform.sh --file $args 02-deadcode.c)" "$(./transform.sh --file $args --enable exp.mincfg 02-deadcode.c)" | sed 's/[[:blank:]]*$//' | tail -n +3
+  @@ -13,0 +14,3 @@
   +  if (n < 0) {
   +    return (0);
   +  }
-  @@ -54,0 +58,2 @@ int one_branch_dead(int x )
+  @@ -54,0 +58,2 @@
   +  } else {
   +    return (7 - x);
-  @@ -65,0 +71,8 @@ int uncalled_but_referenced_function(int
+  @@ -65,0 +71,8 @@
   +int uncalled1(void)
   +{
   +
@@ -227,17 +227,17 @@ Macintosh's diff(1) adds whitespace after the function names, strip with sed.
   +
   +}
   +}
-  @@ -79,0 +93,5 @@ int conditional_call_in_loop(int x )
+  @@ -79,0 +93,5 @@
   +    if (i > 7) {
   +      {
   +      uncalled1();
   +      }
   +    }
-  @@ -151,0 +170,4 @@ int loop_dead_on_break(int z )
+  @@ -151,0 +170,4 @@
   +    {
   +    s += s;
   +    i ++;
   +    }
-  @@ -203,0 +226,2 @@ int main(void)
+  @@ -203,0 +226,2 @@
   +  uncalled1();
   +  uncalled_but_referenced_function(3);

From 166a9b619b87456059de8f1839fb810621302efb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Sep 2023 15:20:48 +0300
Subject: [PATCH 23/42] Add CHANGELOG for v2.2.1

---
 CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 045e06815a..97cc399133 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+## v2.2.1
+* Bump batteries lower bound to 3.5.0.
+* Fix flaky dead code elimination transformation test.
+
 ## v2.2.0
 * Add `setjmp`/`longjmp` analysis (#887, #970, #1015, #1019).
 * Refactor race analysis to lazy distribution (#1084, #1089, #1136, #1016).

From a36572925450fc31fe95f448a75118f004af537a Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Thu, 14 Sep 2023 12:23:21 +0300
Subject: [PATCH 24/42] Add zlib and liblzma functions used in the silver
 searcher

---
 src/analyses/libraryFunctions.ml | 18 ++++++++++++++++++
 src/util/options.schema.json     |  4 +++-
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index e8fabe7dc1..2eb68dd437 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -102,6 +102,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vsprintf", unknown [drop "str" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("mktime", unknown [drop "tm" [r;w]]);
     ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]);
     ("clearerr", unknown [drop "stream" [w]]);
@@ -288,6 +290,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []]); (* TODO: use Call instead of Spawn *)
     ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
     ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
+    ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]);
   ]
 
 (** Pthread functions. *)
@@ -824,6 +827,19 @@ let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pcre_version", unknown []);
   ]
 
+let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("inflate", unknown [drop "strm" [r_deep]; drop "flush" []]);
+    ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]);
+    ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]);
+    ("inflateEnd", unknown [drop "strm" [f_deep]]);
+  ]
+
+let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]);
+    ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]);
+    ("lzma_end", unknown [drop "strm" [r_deep; w_deep]]);
+  ]
+
 let libraries = Hashtbl.of_list [
     ("c", c_descs_list @ math_descs_list);
     ("posix", posix_descs_list);
@@ -837,6 +853,8 @@ let libraries = Hashtbl.of_list [
     ("ncurses", ncurses_descs_list);
     ("zstd", zstd_descs_list);
     ("pcre", pcre_descs_list);
+    ("zlib", zlib_descs_list);
+    ("liblzma", liblzma_descs_list);
   ]
 
 let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 1ef73378fb..1b9c7d3fd5 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1285,7 +1285,9 @@
               "sv-comp",
               "ncurses",
               "zstd",
-              "pcre"
+              "pcre",
+              "zlib",
+              "liblzma"
             ]
           },
           "default": [

From a1464e1ed471aa8fc55b78eae130902da97f1791 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Thu, 14 Sep 2023 21:46:00 +0300
Subject: [PATCH 25/42] Use record as Access.A type instead of a quintuple

---
 src/analyses/raceAnalysis.ml | 33 +++++++++++++++++----------------
 src/domains/access.ml        | 32 ++++++++++++++++++--------------
 2 files changed, 35 insertions(+), 30 deletions(-)

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 74a98af6be..a89ef9206a 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -225,9 +225,9 @@ struct
     | _ ->
       ()
 
-  let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) =
+  let side_access ctx Access.A.{conf; kind; node; exp; acc} ((memoroot, offset) as memo) =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a)))));
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton {conf; kind; node; exp; acc}))));
     side_vars ctx memo
 
   (** Side-effect empty access set for prefix-type_suffix race checking. *)
@@ -302,24 +302,24 @@ struct
         ) (G.vars (ctx.global (V.vars g)))
     | _ -> Queries.Result.top q
 
-  let event ctx e octx =
-    match e with
-    | Events.Access {exp=e; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
+  let event ctx exp octx =
+    match exp with
+    | Events.Access {exp; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       (* must use original (pre-assign, etc) ctx queries *)
       let conf = 110 in
       let module LS = Queries.LS in
       let part_access (vo:varinfo option): MCPAccess.A.t =
         (*partitions & locks*)
-        Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind})))
+        Obj.obj (octx.ask (PartAccess (Memory {exp; var_opt=vo; kind})))
       in
-      let loc = Option.get !Node.current_node in
+      let node = Option.get !Node.current_node in
       let add_access conf voffs =
-        let a = part_access (Option.map fst voffs) in
-        Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs;
+        let acc = part_access (Option.map fst voffs) in
+        Access.add ~side:(side_access octx {conf; kind; node; exp; acc}) ~side_empty:(side_access_empty octx) exp voffs;
       in
       let add_access_struct conf ci =
-        let a = part_access None in
-        Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
+        let acc = part_access None in
+        Access.add_one ~side:(side_access octx {conf; kind; node; exp; acc}) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
       in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls
@@ -345,7 +345,7 @@ struct
           (* the case where the points-to set is non top and contains unknown values *)
           let includes_uk = ref false in
           (* now we need to access all fields that might be pointed to: is this correct? *)
-          begin match octx.ask (ReachableUkTypes e) with
+          begin match octx.ask (ReachableUkTypes exp) with
             | ts when Queries.TS.is_top ts ->
               includes_uk := true
             | ts ->
@@ -370,12 +370,13 @@ struct
     (* perform shallow and deep invalidate according to Library descriptors *)
     let desc = LibraryFunctions.find f in
     if List.mem LibraryDesc.ThreadUnsafe desc.attrs then (
-      let e = Lval (Var f, NoOffset) in
+      let exp = Lval (Var f, NoOffset) in
       let conf = 110 in
-      let loc = Option.get !Node.current_node in
+      let kind = AccessKind.Call in
+      let node = Option.get !Node.current_node in
       let vo = Some f in
-      let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in
-      side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ;
+      let acc = Obj.obj (ctx.ask (PartAccess (Memory {exp; var_opt=vo; kind}))) in
+      side_access ctx {conf; kind; node; exp; acc} ((`Var f), `NoOffset) ;
     );
     ctx.local
 
diff --git a/src/domains/access.ml b/src/domains/access.ml
index 675d1c2e72..05308b5ed9 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -329,12 +329,18 @@ and distribute_access_type f = function
 module A =
 struct
   include Printable.Std
-  type t = int * AccessKind.t * Node.t * CilType.Exp.t * MCPAccess.A.t [@@deriving eq, ord, hash]
+  type t = {
+    conf : int;
+    kind : AccessKind.t;
+    node : Node.t;
+    exp : CilType.Exp.t;
+    acc : MCPAccess.A.t;
+  } [@@deriving eq, ord, hash]
 
   let name () = "access"
 
-  let pretty () (conf, kind, node, e, lp) =
-    Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty e MCPAccess.A.pretty lp
+  let pretty () {conf; kind; node; exp; acc} =
+    Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty exp MCPAccess.A.pretty acc
 
   include Printable.SimplePretty (
     struct
@@ -343,10 +349,8 @@ struct
     end
     )
 
-  let conf (conf, _, _, _, _) = conf
-
-  let relift (conf, kind, node, e, a) =
-    (conf, kind, node, e, MCPAccess.A.relift a)
+  let relift {conf; kind; node; exp; acc} =
+    {conf; kind; node; exp; acc = MCPAccess.A.relift acc}
 end
 
 module AS =
@@ -354,17 +358,17 @@ struct
   include SetDomain.Make (A)
 
   let max_conf accs =
-    accs |> elements |> List.map A.conf |> (List.max ~cmp:Int.compare)
+    accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (List.max ~cmp:Int.compare)
 end
 
 
 (* Check if two accesses may race and if yes with which confidence *)
-let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),loc2,e2,a2) =
+let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} =
   if kind = Read && kind2 = Read then
     false (* two read/read accesses do not race *)
   else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then
     false
-  else if not (MCPAccess.A.may_race a a2) then
+  else if not (MCPAccess.A.may_race acc acc2) then
     false (* analysis-specific information excludes race *)
   else
     true
@@ -487,7 +491,7 @@ let race_conf accs =
   if AS.cardinal accs = 1 then ( (* singleton component *)
     let acc = AS.choose accs in
     if may_race acc acc then (* self-race *)
-      Some (A.conf acc)
+      Some (acc.conf)
     else
       None
   )
@@ -516,9 +520,9 @@ let print_accesses memo grouped_accs =
   let allglobs = get_bool "allglobs" in
   let race_threshold = get_int "warn.race-threshold" in
   let msgs race_accs =
-    let h (conf,kind,node,e,a) =
-      let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty a conf in
-      let doc = dprintf "%t  (exp: %a)" d_msg d_exp e in
+    let h A.{conf; kind; node; exp; acc} =
+      let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty acc conf in
+      let doc = dprintf "%t  (exp: %a)" d_msg d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
     AS.elements race_accs

From 929b658cf26be63fcae41ce3be71499be60a9ebb Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Thu, 14 Sep 2023 21:57:53 +0300
Subject: [PATCH 26/42] Inline d_msg () to doc in access

---
 src/domains/access.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 05308b5ed9..83903ba355 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -521,8 +521,7 @@ let print_accesses memo grouped_accs =
   let race_threshold = get_int "warn.race-threshold" in
   let msgs race_accs =
     let h A.{conf; kind; node; exp; acc} =
-      let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty acc conf in
-      let doc = dprintf "%t  (exp: %a)" d_msg d_exp exp in
+      let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
     AS.elements race_accs

From 60952d933071b651630f6657b133e7625dc5a034 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Fri, 15 Sep 2023 10:34:34 +0300
Subject: [PATCH 27/42] Pass access as a variable instead of destructing the
 record

---
 src/analyses/raceAnalysis.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index a89ef9206a..d1d608ae06 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -225,9 +225,9 @@ struct
     | _ ->
       ()
 
-  let side_access ctx Access.A.{conf; kind; node; exp; acc} ((memoroot, offset) as memo) =
+  let side_access ctx acc ((memoroot, offset) as memo) =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton {conf; kind; node; exp; acc}))));
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton acc))));
     side_vars ctx memo
 
   (** Side-effect empty access set for prefix-type_suffix race checking. *)

From fb7159c0fe7aa1e0ed887f807db7feb3c9699114 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 16 Sep 2023 16:33:40 +0200
Subject: [PATCH 28/42] Add some setjump/longjump test for race detection

---
 tests/regression/68-longjmp/52-races.c        | 36 +++++++++++++
 tests/regression/68-longjmp/53-races-no.c     | 37 ++++++++++++++
 .../regression/68-longjmp/54-races-actually.c | 51 +++++++++++++++++++
 .../68-longjmp/55-races-no-return.c           | 51 +++++++++++++++++++
 4 files changed, 175 insertions(+)
 create mode 100644 tests/regression/68-longjmp/52-races.c
 create mode 100644 tests/regression/68-longjmp/53-races-no.c
 create mode 100644 tests/regression/68-longjmp/54-races-actually.c
 create mode 100644 tests/regression/68-longjmp/55-races-no-return.c

diff --git a/tests/regression/68-longjmp/52-races.c b/tests/regression/68-longjmp/52-races.c
new file mode 100644
index 0000000000..5c7ac6daa6
--- /dev/null
+++ b/tests/regression/68-longjmp/52-races.c
@@ -0,0 +1,36 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <goblint.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   longjmp(env_buffer, 2);
+   pthread_mutex_unlock(&mutex1);
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}
diff --git a/tests/regression/68-longjmp/53-races-no.c b/tests/regression/68-longjmp/53-races-no.c
new file mode 100644
index 0000000000..7247f14941
--- /dev/null
+++ b/tests/regression/68-longjmp/53-races-no.c
@@ -0,0 +1,37 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <goblint.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global ==3) {
+      longjmp(env_buffer, 2);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}
diff --git a/tests/regression/68-longjmp/54-races-actually.c b/tests/regression/68-longjmp/54-races-actually.c
new file mode 100644
index 0000000000..12f1f791c5
--- /dev/null
+++ b/tests/regression/68-longjmp/54-races-actually.c
@@ -0,0 +1,51 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <goblint.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // RACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 3) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //RACE
+   
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}
diff --git a/tests/regression/68-longjmp/55-races-no-return.c b/tests/regression/68-longjmp/55-races-no-return.c
new file mode 100644
index 0000000000..ad0e5d4707
--- /dev/null
+++ b/tests/regression/68-longjmp/55-races-no-return.c
@@ -0,0 +1,51 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <goblint.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 7) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //NORACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}

From 18fe6d1b55fb54f193e1b5ce8506c937ce2d571d Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 16 Sep 2023 16:47:51 +0200
Subject: [PATCH 29/42] 68/[52-55] Don't include `goblint.h`, it is unused

---
 tests/regression/68-longjmp/52-races.c           | 1 -
 tests/regression/68-longjmp/53-races-no.c        | 1 -
 tests/regression/68-longjmp/54-races-actually.c  | 3 +--
 tests/regression/68-longjmp/55-races-no-return.c | 1 -
 4 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/tests/regression/68-longjmp/52-races.c b/tests/regression/68-longjmp/52-races.c
index 5c7ac6daa6..4cde97d954 100644
--- a/tests/regression/68-longjmp/52-races.c
+++ b/tests/regression/68-longjmp/52-races.c
@@ -2,7 +2,6 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <setjmp.h>
-#include <goblint.h>
 #include <pthread.h>
 
 jmp_buf env_buffer;
diff --git a/tests/regression/68-longjmp/53-races-no.c b/tests/regression/68-longjmp/53-races-no.c
index 7247f14941..4692f6ca18 100644
--- a/tests/regression/68-longjmp/53-races-no.c
+++ b/tests/regression/68-longjmp/53-races-no.c
@@ -2,7 +2,6 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <setjmp.h>
-#include <goblint.h>
 #include <pthread.h>
 
 jmp_buf env_buffer;
diff --git a/tests/regression/68-longjmp/54-races-actually.c b/tests/regression/68-longjmp/54-races-actually.c
index 12f1f791c5..62423cd884 100644
--- a/tests/regression/68-longjmp/54-races-actually.c
+++ b/tests/regression/68-longjmp/54-races-actually.c
@@ -2,7 +2,6 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <setjmp.h>
-#include <goblint.h>
 #include <pthread.h>
 
 jmp_buf env_buffer;
@@ -44,7 +43,7 @@ int main() {
    }
 
    global = 5; //RACE
-   
+
    if(n == 0) {
       pthread_mutex_unlock(&mutex1);
    }
diff --git a/tests/regression/68-longjmp/55-races-no-return.c b/tests/regression/68-longjmp/55-races-no-return.c
index ad0e5d4707..850fc54fa5 100644
--- a/tests/regression/68-longjmp/55-races-no-return.c
+++ b/tests/regression/68-longjmp/55-races-no-return.c
@@ -2,7 +2,6 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <setjmp.h>
-#include <goblint.h>
 #include <pthread.h>
 
 jmp_buf env_buffer;

From 1feb75e2aa06ccacec63b39e52cfc0661b5d9a80 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 18 Sep 2023 11:31:51 +0300
Subject: [PATCH 30/42] Fix Cilfacade.split_anoncomp_name for empty names
 (closes #1171)

---
 src/domains/access.ml          |  4 ++--
 src/util/cilfacade.ml          |  9 +++++----
 unittest/mainTest.ml           |  1 +
 unittest/util/cilfacadeTest.ml | 14 ++++++++++++++
 4 files changed, 22 insertions(+), 6 deletions(-)
 create mode 100644 unittest/util/cilfacadeTest.ml

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 83903ba355..fa6446df16 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -16,8 +16,8 @@ let is_ignorable_type (t: typ): bool =
   | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true
   | TComp ({ cname; _}, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with
-      | (true, ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
-      | (false, ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
+      | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
+      | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
       | _ -> false
     end
   | TComp ({ cname = "lock_class_key"; _ }, _) -> true
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index c77d2cd738..f0ac3202ce 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -342,22 +342,23 @@ let makeBinOp binop e1 e2 =
   let (_, e) = Cabs2cil.doBinOp binop e1 t1 e2 t2 in
   e
 
-let anoncomp_name_regexp = Str.regexp {|^__anon\(struct\|union\)_\(.+\)_\([0-9]+\)$|}
+let anoncomp_name_regexp = Str.regexp {|^__anon\(struct\|union\)\(_\(.+\)\)?_\([0-9]+\)$|}
 
 let split_anoncomp_name name =
   (* __anonunion_pthread_mutexattr_t_488594144 *)
+  (* __anonunion_50 *)
   if Str.string_match anoncomp_name_regexp name 0 then (
     let struct_ = match Str.matched_group 1 name with
       | "struct" -> true
       | "union" -> false
       | _ -> assert false
     in
-    let name' = Str.matched_group 2 name in
-    let id = int_of_string (Str.matched_group 3 name) in
+    let name' = try Some (Str.matched_group 3 name) with Not_found -> None in
+    let id = int_of_string (Str.matched_group 4 name) in
     (struct_, name', id)
   )
   else
-    invalid_arg "Cilfacade.split_anoncomp_name"
+    invalid_arg ("Cilfacade.split_anoncomp_name: " ^ name)
 
 (** Pretty-print typsig like typ, because
     {!d_typsig} prints with CIL constructors. *)
diff --git a/unittest/mainTest.ml b/unittest/mainTest.ml
index df67340309..642e495d50 100644
--- a/unittest/mainTest.ml
+++ b/unittest/mainTest.ml
@@ -8,6 +8,7 @@ let all_tests = ("" >:::
     LvalTest.test ();
     CompilationDatabaseTest.tests;
     LibraryDslTest.tests;
+    CilfacadeTest.tests;
     (* etc *)
     "domaintest" >::: QCheck_ounit.to_ounit2_test_list Maindomaintest.all_testsuite;
     IntOpsTest.tests;
diff --git a/unittest/util/cilfacadeTest.ml b/unittest/util/cilfacadeTest.ml
new file mode 100644
index 0000000000..482a502824
--- /dev/null
+++ b/unittest/util/cilfacadeTest.ml
@@ -0,0 +1,14 @@
+open Goblint_lib
+open OUnit2
+open Cilfacade
+
+let test_split_anoncomp_name _ =
+  let assert_equal = assert_equal ~printer:[%show: bool * string option * int] in
+  assert_equal (false, Some "pthread_mutexattr_t", 488594144) (split_anoncomp_name "__anonunion_pthread_mutexattr_t_488594144");
+  assert_equal (true, Some "__once_flag", 1234) (split_anoncomp_name "__anonstruct___once_flag_1234");
+  assert_equal (false, None, 50) (split_anoncomp_name "__anonunion_50")
+
+let tests =
+  "cilfacadeTest" >::: [
+    "split_anoncomp_name" >:: test_split_anoncomp_name;
+  ]

From 444428467d44a3d188d034c4418d34117543b838 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 18 Sep 2023 11:36:23 +0300
Subject: [PATCH 31/42] Remove duplicate vsprintf and add vsnprintf

---
 src/analyses/libraryFunctions.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 2eb68dd437..912867d319 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -103,7 +103,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
-    ("vsprintf", unknown [drop "str" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("mktime", unknown [drop "tm" [r;w]]);
     ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]);
     ("clearerr", unknown [drop "stream" [w]]);
@@ -1089,7 +1089,6 @@ let invalidate_actions = [
     "usleep", readsAll;
     "svc_run", writesAll;(*unsafe*)
     "dup", readsAll; (*safe*)
-    "vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
     "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
     "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
     "strcasecmp", readsAll; (*safe*)

From 684cfa8c3f45afcefd95a1096e954fad27af8d91 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com>
Date: Mon, 18 Sep 2023 11:37:22 +0300
Subject: [PATCH 32/42] Apply suggestions from code review

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/analyses/libraryFunctions.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 912867d319..b883c7e354 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -828,7 +828,7 @@ let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
   ]
 
 let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
-    ("inflate", unknown [drop "strm" [r_deep]; drop "flush" []]);
+    ("inflate", unknown [drop "strm" [r_deep; w_deep]; drop "flush" []]);
     ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]);
     ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]);
     ("inflateEnd", unknown [drop "strm" [f_deep]]);
@@ -837,7 +837,7 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]);
     ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]);
-    ("lzma_end", unknown [drop "strm" [r_deep; w_deep]]);
+    ("lzma_end", unknown [drop "strm" [r_deep; w_deep; f_deep]]);
   ]
 
 let libraries = Hashtbl.of_list [

From e69d13c0cd4cf73a9bbda511627ee1844a39bbbc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 18 Sep 2023 11:49:06 +0300
Subject: [PATCH 33/42] Add thread self creation non-terminating test from
 libaco

---
 tests/regression/10-synch/07-thread_self_create.c | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 tests/regression/10-synch/07-thread_self_create.c

diff --git a/tests/regression/10-synch/07-thread_self_create.c b/tests/regression/10-synch/07-thread_self_create.c
new file mode 100644
index 0000000000..473a26a25b
--- /dev/null
+++ b/tests/regression/10-synch/07-thread_self_create.c
@@ -0,0 +1,15 @@
+// PARAM: --set ana.activated[+] thread
+// Checks termination of thread analysis with a thread who is its own single parent.
+#include <pthread.h>
+
+void *t_fun(void *arg) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  return 0;
+}

From 2486404315e4e7d44512134637d1eaff78def99e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 18 Sep 2023 11:55:59 +0300
Subject: [PATCH 34/42] Fix 10-synch/07-thread_self_create

---
 src/analyses/threadAnalysis.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index d6a93744bc..1e679a4707 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -32,13 +32,21 @@ struct
 
   let rec is_not_unique ctx tid =
     let (rep, parents, _) = ctx.global tid in
-    let n = TS.cardinal parents in
-    (* A thread is not unique if it is
-      * a) repeatedly created,
-      * b) created in multiple threads, or
-      * c) created by a thread that is itself multiply created.
-      * Note that starting threads have empty ancestor sets! *)
-    rep || n > 1 || n > 0 && is_not_unique ctx (TS.choose parents)
+    if rep then
+      true (* repeatedly created *)
+    else (
+      let n = TS.cardinal parents in
+      if n > 1 then
+        true (* created in multiple threads *)
+      else if n > 0 then (
+        (* created by single thread *)
+        let parent = TS.choose parents in
+        (* created by itself thread-recursively or by a thread that is itself multiply created *)
+        T.equal tid parent || is_not_unique ctx parent (* equal check needed to avoid infinte self-recursion *)
+      )
+      else
+        false (* no ancestors, starting thread *)
+    )
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in

From 0f59ac967b1fd37bbea7c6c4c2a785a136f36c03 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 19 Sep 2023 13:50:10 +0300
Subject: [PATCH 35/42] Fix Cilfacade.pretty_typsig_like_typ forgetting
 pointers from name on base type

---
 src/util/cilfacade.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index f0ac3202ce..eb7330aa19 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -377,7 +377,7 @@ let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
     | _ -> pa
   in
   match ts with
-  | TSBase t -> dn_type () t
+  | TSBase t -> defaultCilPrinter#pType nameOpt () t
   | TSComp (cstruct, cname, a) ->
     let su = if cstruct then "struct" else "union" in
     text (su ^ " " ^ cname ^ " ")

From d0e9064924f4548d4ac5fc277d5644cbbddcfcf3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 19 Sep 2023 21:49:05 +0200
Subject: [PATCH 36/42] Fix `trace` calls outside of `if tracing`

---
 src/solvers/sLRphased.ml |  8 ++++----
 src/solvers/sLRterm.ml   | 12 ++++++------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml
index f4c3389f1d..c120a7bc6c 100644
--- a/src/solvers/sLRphased.ml
+++ b/src/solvers/sLRphased.ml
@@ -73,7 +73,7 @@ module Make =
         let effects = ref Set.empty in
         let side y d =
           assert (not (S.Dom.is_bot d));
-          trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -109,11 +109,11 @@ module Make =
           if wpx then
             if b then
               let nar = narrow old tmp in
-              trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar
             else
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
               wid
           else
             tmp
@@ -163,7 +163,7 @@ module Make =
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = Enum.fold (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.enum w)
-        in trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
+        in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
       and eq x get set =
         eval_rhs_event x;
         match S.system x with
diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml
index d4f4671c46..eb11447d11 100644
--- a/src/solvers/sLRterm.ml
+++ b/src/solvers/sLRterm.ml
@@ -64,14 +64,14 @@ module SLR3term =
           HM.replace rho  x (S.Dom.bot ());
           HM.replace infl x (VS.add x VS.empty);
           let c = if side then count_side else count in
-          trace "sol" "INIT: Var: %a with prio %d\n" S.Var.pretty_trace x !c;
+          if tracing then trace "sol" "INIT: Var: %a with prio %d\n" S.Var.pretty_trace x !c;
           HM.replace key x !c; decr c
         end
       in
       let sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = Enum.fold (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.enum w) in
-        trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
+        if tracing then trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
       in
       let rec iterate b_old prio =
         if H.size !q = 0 || min_key q > prio then ()
@@ -122,7 +122,7 @@ module SLR3term =
           )
           *)
           (* if S.Dom.is_bot d then print_endline "BOT" else *)
-          trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -156,17 +156,17 @@ module SLR3term =
           if wpx then
             if S.Dom.leq tmp old then (
               let nar = narrow old tmp in
-              trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar, true
             ) else
             if b_old then (
               let nar = narrow old tmp in
-              trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar, true
             )
             else (
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
               wid, false
             )
           else

From 8336d28999086a3ae18b8c6cbd976ea916bde07d Mon Sep 17 00:00:00 2001
From: sallto <68823230+sallto@users.noreply.github.com>
Date: Sat, 23 Sep 2023 16:38:26 +0200
Subject: [PATCH 37/42] fix: copying of files to GobView in projects with
 subdirectories (#1143)

* fix: macos command line file

* fix: special paths for macos and non-english languages

special paths are os and language dependant.
ex. <command-line> -> <command line> for macos

* fix: prevent recursive directory copies when using gobview

* fix: correct counter for gobview files
Counter for unique file names was broken by skipping directory entries

* fix: remove unnecessary recursive copying

---------

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 src/maingoblint.ml | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 8944d87ea0..155faa0e76 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -417,10 +417,9 @@ let parse_preprocessed preprocessed =
 
   let goblint_cwd = GobFpath.cwd () in
   let get_ast_and_record_deps (preprocessed_file, task_opt) =
-    let transform_file (path_str, system_header) = match path_str with
-      | "<built-in>" | "<command-line>" ->
+    let transform_file (path_str, system_header) = if Str.string_match (Str.regexp "<.+>") path_str 0 then
         (path_str, system_header) (* ignore special "paths" *)
-      | _ ->
+      else
         let path = Fpath.v path_str in
         let path' = if get_bool "pre.transform-paths" then (
             let cwd_opt =
@@ -584,19 +583,19 @@ let do_gobview cilfile =
       let file_dir = Fpath.(run_dir / "files") in
       GobSys.mkdir_or_exists file_dir;
       let file_loc = Hashtbl.create 113 in
-      let counter = ref 0 in
-      let copy path =
+      let copy (path, i) =
         let name, ext = Fpath.split_ext (Fpath.base path) in
-        let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int !counter) name) in
-        counter := !counter + 1;
+        let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int i) name) in
         let dest = Fpath.(file_dir // unique_name) in
         let gobview_path = match Fpath.relativize ~root:run_dir dest with
           | Some p -> Fpath.to_string p
           | None -> failwith "The gobview directory should be a prefix of the paths of c files copied to the gobview directory" in
         Hashtbl.add file_loc (Fpath.to_string path) gobview_path;
-        FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest) in
+        FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest)
+      in
       let source_paths = Preprocessor.FpathH.to_list Preprocessor.dependencies |> List.concat_map (fun (_, m) -> Fpath.Map.fold (fun p _ acc -> p::acc) m []) in
-      List.iter copy source_paths;
+      let source_file_paths = List.filteri_map (fun i e -> if Fpath.is_file_path e then Some (e, i) else None) source_paths in
+      List.iter copy source_file_paths;
       Serialize.marshal file_loc (Fpath.(run_dir / "file_loc.marshalled"));
       (* marshal timing statistics *)
       let stats = Fpath.(run_dir / "stats.marshalled") in

From 70f267b1bb50c66a0e0332982506de963c6f619e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 25 Sep 2023 10:36:12 +0300
Subject: [PATCH 38/42] Add more categories to unsound/imprecise call messages

---
 src/analyses/base.ml         | 6 +++---
 src/framework/constraints.ml | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 71e2661997..aac369fed3 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1104,12 +1104,12 @@ struct
       if AD.mem Addr.UnknownPtr fp then begin
         let others = AD.to_var_may fp in
         if others = [] then raise OnlyUnknown;
-        M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;
+        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval;
         dummyFunDec.svar :: others
       end else
         AD.to_var_may fp
     with SetDomain.Unsupported _ | OnlyUnknown ->
-      M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;
+      M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval;
       [dummyFunDec.svar]
 
   (** Evaluate expression as address.
@@ -1970,7 +1970,7 @@ struct
     end
 
   let special_unknown_invalidate ctx ask gs st f args =
-    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise "Unknown function ptr called");
+    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called");
     let desc = LF.find f in
     let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
     let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 740d1f85a9..288b7ad0ea 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -776,16 +776,16 @@ struct
           end
         else begin
           let geq = if var_arg then ">=" else "" in
-          M.warn ~tags:[CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
+          M.warn ~category:Unsound ~tags:[Category Call; CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
           None
         end
       | _ ->
-        M.warn  ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
+        M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
         None
     in
     let funs = List.filter_map one_function functions in
     if [] = funs then begin
-      M.warn ~category:Unsound "No suitable function to be called at call site. Continuing with state before call.";
+      M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call.";
       d (* because LevelSliceLifter *)
     end else
       common_joins ctx funs !r !spawns

From 16077e3b146d464072004eaf0cd1480a2a7b99d1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 25 Sep 2023 13:27:33 +0300
Subject: [PATCH 39/42] Add region interprocedural fixpoint error test

---
 .../09-regions/40-zstd-thread-pool-region.c   | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 tests/regression/09-regions/40-zstd-thread-pool-region.c

diff --git a/tests/regression/09-regions/40-zstd-thread-pool-region.c b/tests/regression/09-regions/40-zstd-thread-pool-region.c
new file mode 100644
index 0000000000..13baf5ec3f
--- /dev/null
+++ b/tests/regression/09-regions/40-zstd-thread-pool-region.c
@@ -0,0 +1,34 @@
+// SKIP PARAM: --set ana.activated[+] region
+// FIXPOINT
+#include<stdlib.h>
+#include<pthread.h>
+#include<goblint.h>
+
+typedef struct POOL_job_s {
+    void *opaque;
+} POOL_job;
+
+typedef struct POOL_ctx_s {
+    POOL_job *queue;
+} POOL_ctx;
+
+POOL_ctx* ctx_global;
+
+POOL_ctx* POOL_create(size_t numThreads, size_t queueSize)
+{
+    POOL_ctx* ctx_create;
+    ctx_create = (POOL_ctx*)malloc(sizeof(POOL_ctx));
+    ctx_create->queue = (POOL_job*)malloc(queueSize * sizeof(POOL_job));
+
+    int r; // rand
+    if (r)
+        ctx_global = ctx_create; // pretend escape
+    return ctx_create;
+}
+
+int main() {
+    while (1) {
+        POOL_ctx *ctx_main;
+        ctx_main = POOL_create(20, 10);
+    }
+}

From 23a5d83ab8a1af6431a9c00934139ff056758642 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 25 Sep 2023 16:30:25 +0300
Subject: [PATCH 40/42] Add eqd to TD3 tracing output

---
 src/solvers/td3.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 29ad301292..07edc632c7 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -327,7 +327,7 @@ module Base =
               else
                 box old eqd
           in
-          if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty wpd;
+          if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd;
           if cache then (
             if tracing then trace "cache" "cache size %d for %a\n" (HM.length l) S.Var.pretty_trace x;
             cache_sizes := HM.length l :: !cache_sizes;

From 810fab57274821d600b5d841a8a1be977311a3b2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 25 Sep 2023 17:36:12 +0300
Subject: [PATCH 41/42] Add zstd unsound both branches dead test

---
 .../03-practical/31-zstd-cctxpool-blobs.c     | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/regression/03-practical/31-zstd-cctxpool-blobs.c

diff --git a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
new file mode 100644
index 0000000000..40e448eb22
--- /dev/null
+++ b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
@@ -0,0 +1,29 @@
+#include <stdlib.h>
+#include <pthread.h>
+
+struct ZSTD_CCtx_s {
+  int bmi2;
+};
+
+typedef struct ZSTD_CCtx_s ZSTD_CCtx;
+
+typedef struct {
+  ZSTD_CCtx* cctx[1];
+} ZSTDMT_CCtxPool;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
+
+  ZSTDMT_CCtxPool* const cctxPool = calloc(1, sizeof(ZSTDMT_CCtxPool));
+  cctxPool->cctx[0] = malloc(sizeof(ZSTD_CCtx));
+  if (!cctxPool->cctx[0]) // TODO NOWARN
+    __goblint_check(1); // TODO reachable
+  else
+    __goblint_check(1); // TODO reachable
+  return 0;
+}

From 5347c087b4eec4c7db77832b2c4f97c7d2841598 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 26 Sep 2023 11:22:12 +0300
Subject: [PATCH 42/42] Add eval_offset tracing

---
 src/cdomains/valueDomain.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 9d894b6b34..cba4b04c18 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -824,6 +824,8 @@ struct
   (* Funny, this does not compile without the final type annotation! *)
   let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
     let rec do_eval_offset (ask:VDQ.t) f (x:t) (offs:offs) (exp:exp option) (l:lval option) (o:offset option) (v:lval option) (t:typ): t =
+      if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp;
+      let r =
       match x, offs with
       | Blob((va, _, orig) as c), `Index (_, ox) ->
         begin
@@ -886,6 +888,9 @@ struct
             | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
             | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
           end
+      in
+      if M.tracing then M.traceu "eval_offset" "do_eval_offset -> %a\n" pretty r;
+      r
     in
     let l, o = match exp with
       | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)