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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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 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 28/30] 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 29/30] 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 30/30] 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 [