From 884763609adc2e457727d089745c679a4d42a7be Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Fri, 9 Jun 2023 21:38:44 +0300
Subject: [PATCH 01/55] Add (function) Call to accessKind

---
 src/analyses/libraryFunctions.ml | 23 ++++++++++++-----------
 src/analyses/mutexAnalysis.ml    |  1 +
 src/domains/accessKind.ml        |  4 +++-
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 9b689b64ad..31ed3adb65 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -797,70 +797,70 @@ struct
 
   let writesAllButFirst n f a x =
     match a with
-    | Write | Spawn -> f a x @ drop n x
+    | Write | Call | Spawn -> f a x @ drop n x
     | Read  -> f a x
     | Free  -> []
 
   let readsAllButFirst n f a x =
     match a with
-    | Write | Spawn -> f a x
+    | Write | Call | Spawn -> f a x
     | Read  -> f a x @ drop n x
     | Free  -> []
 
   let reads ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> o
+    | Write | Call | Spawn -> o
     | Read  -> i
     | Free  -> []
 
   let writes ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> i
+    | Write | Call | Spawn -> i
     | Read  -> o
     | Free  -> []
 
   let frees ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> o
     | Free  -> i
 
   let readsFrees rs fs a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> keep rs x
     | Free  -> keep fs x
 
   let onlyReads ns a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> keep ns x
     | Free  -> []
 
   let onlyWrites ns a x =
     match a with
-    | Write | Spawn -> keep ns x
+    | Write | Call | Spawn -> keep ns x
     | Read  -> []
     | Free  -> []
 
   let readsWrites rs ws a x =
     match a with
-    | Write | Spawn -> keep ws x
+    | Write | Call | Spawn -> keep ws x
     | Read  -> keep rs x
     | Free  -> []
 
   let readsAll a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> x
     | Free  -> []
 
   let writesAll a x =
     match a with
-    | Write | Spawn -> x
+    | Write | Call | Spawn -> x
     | Read  -> []
     | Free  -> []
 end
@@ -1158,6 +1158,7 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
     | Read when GobConfig.get_bool "sem.unknown_function.read.args" -> args
     | Read -> []
     | Free -> []
+    | Call -> [] (* TODO: option *)
     | Spawn when get_bool "sem.unknown_function.spawn" -> args
     | Spawn -> []
   in
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 9029c1b4a1..6d39be150c 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -254,6 +254,7 @@ struct
             let write = match kind with
               | Write | Free -> true
               | Read -> false
+              | Call
               | Spawn -> false (* TODO: nonsense? *)
             in
             let s = GProtecting.make ~write ~recovered:is_recovered_to_st locks in
diff --git a/src/domains/accessKind.ml b/src/domains/accessKind.ml
index 576581af02..b36e8f3eca 100644
--- a/src/domains/accessKind.ml
+++ b/src/domains/accessKind.ml
@@ -1,9 +1,10 @@
 (** Kinds of memory accesses. *)
 
 type t =
-  | Write  (** argument may be read or written to *)
+  | Write  (** argument may be written to *)
   | Read   (** argument may be read *)
   | Free   (** argument may be freed *)
+  | Call   (** argument may be called *)
   | Spawn  (** argument may be spawned *)
 [@@deriving eq, ord, hash]
 (** Specifies what is known about an argument. *)
@@ -12,6 +13,7 @@ let show: t -> string = function
   | Write -> "write"
   | Read -> "read"
   | Free -> "free"
+  | Call -> "call"
   | Spawn -> "spawn"
 
 include Printable.SimpleShow (

From d58c1ca6e0182b86daf083180d986aa52315654b Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Fri, 9 Jun 2023 22:17:30 +0300
Subject: [PATCH 02/55] Add tests for thread-unsafe function call

---
 .../04-mutex/77-thread-unsafe_fun_rc.c        | 22 +++++++++++++++++++
 .../04-mutex/78-thread-unsafe_fun_nr.c        | 21 ++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 tests/regression/04-mutex/77-thread-unsafe_fun_rc.c
 create mode 100644 tests/regression/04-mutex/78-thread-unsafe_fun_nr.c

diff --git a/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c
new file mode 100644
index 0000000000..8f2f01fc6d
--- /dev/null
+++ b/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c
@@ -0,0 +1,22 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  rand(); // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  rand(); // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/04-mutex/78-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/78-thread-unsafe_fun_nr.c
new file mode 100644
index 0000000000..df02d23db9
--- /dev/null
+++ b/tests/regression/04-mutex/78-thread-unsafe_fun_nr.c
@@ -0,0 +1,21 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  rand(); // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex1);
+  rand(); // NORACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}

From 874c1864bc2f4e4cdc14138de09c9a408c94f319 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Fri, 9 Jun 2023 22:18:38 +0300
Subject: [PATCH 03/55] Handle thread-unsafe function calls in raceAnalysis
 #723

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

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 481ccbf60b..30cf03cfa7 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -153,6 +153,19 @@ struct
     | _ ->
       ctx.local
 
+  let special ctx (lvalOpt: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    (* 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 conf = 110 in
+      let loc = 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 (`Type f.vtype) (Some (f, `NoOffset)) (conf, Call, loc, e, a);
+    );
+    ctx.local
+
   let finalize () =
     let total = !safe + !unsafe + !vulnerable in
     if total > 0 then (

From 027b9cda653b95e63f904b417256da1b476546bb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Aug 2023 11:41:35 +0300
Subject: [PATCH 04/55] Improve solside tracing

---
 src/framework/analyses.ml | 1 +
 src/solvers/td3.ml        | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index dd57f40c70..df3346af93 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -75,6 +75,7 @@ end
 module GVarF (V: SpecSysVar) =
 struct
   include Printable.Either (V) (CilType.Fundec)
+  let name () = "FromSpec"
   let spec x = `Left x
   let contexts x = `Right x
 
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index f0a728f73b..9621f69db8 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -429,7 +429,7 @@ module Base =
         if tracing then trace "sol2" "stable add %a\n" S.Var.pretty_trace y;
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
-          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x;
+          if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a: %a -> %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp;
           let sided = match x with
             | Some x ->
               let sided = VS.mem x old_sides in

From 152f34eebcc29471f43f4f7f49597b4b64fa5354 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Aug 2023 11:43:07 +0300
Subject: [PATCH 05/55] Handle all_index in evalbinop_base

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 1808014654..5b7a16e002 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -397,6 +397,8 @@ struct
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
         | Ne ->
           Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
+        | IndexPI when AD.to_string p2 = ["all_index"] ->
+          addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
         | _ -> VD.top ()
       end
     (* For other values, we just give up! *)

From 6d0498326c395d35d51b23df9d754b866ff0fe7f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Aug 2023 11:43:35 +0300
Subject: [PATCH 06/55] Improve widen tracing

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

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index b1db3796a8..5417598360 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -760,7 +760,7 @@ struct
       norm ik @@ Some (l2,u2) |> fst
   let widen ik x y =
     let r = widen ik x y in
-    if M.tracing then M.tracel "int" "interval widen %a %a -> %a\n" pretty x pretty y pretty r;
+    if M.tracing && not (equal x y) then M.tracel "int" "interval widen %a %a -> %a\n" pretty x pretty y pretty r;
     assert (leq x y); (* TODO: remove for performance reasons? *)
     r
 
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 9621f69db8..26df6aac95 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -334,6 +334,8 @@ module Base =
           );
           if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* value changed *)
             if tracing then trace "sol" "Changed\n";
+            (* if tracing && not (S.Dom.is_bot old) && HM.mem wpoint x then trace "solchange" "%a (wpx: %b): %a -> %a\n" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty old S.Dom.pretty wpd; *)
+            if tracing && not (S.Dom.is_bot old) && HM.mem wpoint x then trace "solchange" "%a (wpx: %b): %a\n" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
             HM.replace rho x wpd;
             destabilize x;

From f0a05668ca991baa67ad5eadf4b722357bca263b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 18 May 2023 17:18:38 +0300
Subject: [PATCH 07/55] Fix var_eq may_change for other argument being constant

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

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 99307d5d37..3054f2e0da 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -291,7 +291,7 @@ struct
            | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let r =
-      if Cil.isConstant b then false
+      if Cil.isConstant b || Cil.isConstant a then false
       else if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
       then ((*Messages.warn ~category:Analyzer "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.LS.exists (lval_may_change_pt a) bls

From 5372a76b0b2dad8a89193cbcc14e0c2ff33e0945 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 19 May 2023 13:46:38 +0300
Subject: [PATCH 08/55] Disable CIL check in unassume because variables of
 typedef types fail

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

diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 6b719c57b9..43707acd1e 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -111,7 +111,7 @@ struct
           Locator.ES.iter (fun n ->
               let fundec = Node.find_fundec n in
 
-              match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                 NH.add invs n {exp = inv_exp; uuid}
@@ -157,12 +157,12 @@ struct
           Locator.ES.iter (fun n ->
               let fundec = Node.find_fundec n in
 
-              match InvariantParser.parse_cil inv_parser ~fundec ~loc pre_cabs with
+              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc pre_cabs with
               | Ok pre_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located precondition to %a: %a" CilType.Fundec.pretty fundec Cil.d_exp pre_exp;
                 FH.add fun_pres fundec pre_exp;
 
-                begin match InvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs with
+                begin match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
                   | Ok inv_exp ->
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then

From 10881f05c6318ed501249986858b80a5c49f0c70 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 19 May 2023 13:46:50 +0300
Subject: [PATCH 09/55] Add solchange tracing to TD3 side effects

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

diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 26df6aac95..29ad301292 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -432,6 +432,7 @@ module Base =
         HM.replace stable y ();
         if not (S.Dom.leq tmp old) then (
           if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a: %a -> %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp;
+          if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %b) from %a: %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old);
           let sided = match x with
             | Some x ->
               let sided = VS.mem x old_sides in

From 90f155cb23bffb2ca55d1d26dc2df5dd1c8a4035 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Sat, 20 May 2023 11:04:56 +0300
Subject: [PATCH 10/55] Exclude more pthread types from base

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

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 20c4f3bf21..9d8fcc5012 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -115,7 +115,7 @@ struct
     | _ -> false
 
   let is_mutex_type (t: typ): bool = match t with
-    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t"
+    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t" || info.tname = "pthread_mutexattr_t"
     | TInt (IInt, attr) -> hasAttribute "mutex" attr
     | _ -> false
 

From 5e19b23189b80012c6571b669b4233945036ae0b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 1 Aug 2023 12:00:01 +0300
Subject: [PATCH 11/55] Fix relational witness literature examples to also
 validate

---
 tests/regression/56-witness/37-hh-ex3.c        | 2 +-
 tests/regression/56-witness/37-hh-ex3.yml      | 4 ++--
 tests/regression/56-witness/40-bh-ex1-poly.yml | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/regression/56-witness/37-hh-ex3.c b/tests/regression/56-witness/37-hh-ex3.c
index c3f26b5cf1..e59fd53108 100644
--- a/tests/regression/56-witness/37-hh-ex3.c
+++ b/tests/regression/56-witness/37-hh-ex3.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.apron.strengthening --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/37-hh-ex3.yml b/tests/regression/56-witness/37-hh-ex3.yml
index 9a4562d6d2..d6cd5150a4 100644
--- a/tests/regression/56-witness/37-hh-ex3.yml
+++ b/tests/regression/56-witness/37-hh-ex3.yml
@@ -20,10 +20,10 @@
   location:
     file_name: 37-hh-ex3.c
     file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
-    line: 7
+    line: 6
     column: 4
     function: main
   location_invariant:
-    string: 0 <= i && i <= 3 && j == 0
+    string: 0 <= i && i <= 3
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/40-bh-ex1-poly.yml b/tests/regression/56-witness/40-bh-ex1-poly.yml
index e219e1f877..cdbd8d666b 100644
--- a/tests/regression/56-witness/40-bh-ex1-poly.yml
+++ b/tests/regression/56-witness/40-bh-ex1-poly.yml
@@ -20,10 +20,10 @@
   location:
     file_name: 40-bh-ex1-poly.c
     file_hash: 34f781dcae089ecb6b7b2811027395fcb501b8477b7e5016f7b38081724bea28
-    line: 8
+    line: 7
     column: 4
     function: main
   location_invariant:
-    string: 0 <= i && i <= 3 && j == 0
+    string: 0 <= i && i <= 3
     type: assertion
     format: C

From e018cb756ab36ac6f4a27d6056fd08305216435a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 1 Aug 2023 14:57:25 +0300
Subject: [PATCH 12/55] Add non-terminating hh-ex3

---
 src/cdomains/apron/apronDomain.apron.ml       |  6 ++--
 src/goblint.ml                                |  2 +-
 tests/regression/56-witness/63-hh-ex3-term.c  | 33 +++++++++++++++++++
 .../regression/56-witness/63-hh-ex3-term.yml  | 25 ++++++++++++++
 4 files changed, 62 insertions(+), 4 deletions(-)
 create mode 100644 tests/regression/56-witness/63-hh-ex3-term.c
 create mode 100644 tests/regression/56-witness/63-hh-ex3-term.yml

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d9928df597..7dffafe967 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -693,16 +693,16 @@ struct
 
   let join x y =
     (* just to optimize joining folds, which start with bot *)
-    if is_bot x then
+    if is_bot x then (* TODO: also for non-empty env *)
       y
-    else if is_bot y then
+    else if is_bot y then (* TODO: also for non-empty env *)
       x
     else (
       if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y;
       let j = join x y in
       if M.tracing then M.trace "apron" "j = %a\n" pretty j;
       let j =
-        if strengthening_enabled then
+        if strengthening_enabled then (* TODO: skip if same envs? *)
           strengthening j x y
         else
           j
diff --git a/src/goblint.ml b/src/goblint.ml
index a73d0a9fad..4ea3a3d242 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -73,7 +73,7 @@ let main () =
     exit 1
   | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *)
     do_stats ();
-    (* Printexc.print_backtrace BatInnerIO.stderr *)
+    Printexc.print_backtrace stderr;
     eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
     Goblint_timing.teardown_tef ();
     exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *)
diff --git a/tests/regression/56-witness/63-hh-ex3-term.c b/tests/regression/56-witness/63-hh-ex3-term.c
new file mode 100644
index 0000000000..0d90e8753f
--- /dev/null
+++ b/tests/regression/56-witness/63-hh-ex3-term.c
@@ -0,0 +1,33 @@
+// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron --set ana.apron.domain polyhedra --enable ana.apron.strengthening --set ana.activated[+] unassume --set witness.yaml.unassume 63-hh-ex3-term.yml --enable ana.widen.tokens --disable witness.invariant.other --enable exp.arg
+extern void __assert_fail (const char *__assertion, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert_perror_fail (int __errnum, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert (const char *__assertion, const char *__file, int __line)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+
+extern void abort(void);
+void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "hh-ex3.c", 3, __extension__ __PRETTY_FUNCTION__); })); }
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+int main() {
+  int i = 0;
+  while (i < 4) {
+    int j = 0;
+    while (j < 4) {
+      i++;
+      j++;
+      __VERIFIER_assert(0 <= j);
+      __VERIFIER_assert(j <= i);
+      __VERIFIER_assert(i <= j + 3);
+      __VERIFIER_assert(j <= 4);
+    }
+    __VERIFIER_assert(0 <= j);
+    __VERIFIER_assert(j <= i);
+    __VERIFIER_assert(i <= j + 3);
+    __VERIFIER_assert(j <= 4);
+    i = i - j + 1;
+  }
+  return 0;
+}
diff --git a/tests/regression/56-witness/63-hh-ex3-term.yml b/tests/regression/56-witness/63-hh-ex3-term.yml
new file mode 100644
index 0000000000..e635e24014
--- /dev/null
+++ b/tests/regression/56-witness/63-hh-ex3-term.yml
@@ -0,0 +1,25 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: d834761a-d0d7-4fea-bf42-2ff2b9a19143
+    creation_time: 2022-10-12T10:59:25Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - /home/vagrant/eval-prec/prec/hh-ex3.i
+      input_file_hashes:
+        /home/vagrant/eval-prec/prec/hh-ex3.i: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+      data_model: LP64
+      language: C
+  location:
+    file_name: 63-hh-ex3-term.c
+    file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+    line: 17
+    column: 4
+    function: main
+  location_invariant:
+    string: 0 <= i && i <= 3
+    type: assertion
+    format: C

From 0715a0451a6069368370aac1a6deeb29f2b3da36 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 1 Aug 2023 15:45:12 +0300
Subject: [PATCH 13/55] Simplify hh-ex3-term

---
 tests/regression/56-witness/63-hh-ex3-term.c | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/tests/regression/56-witness/63-hh-ex3-term.c b/tests/regression/56-witness/63-hh-ex3-term.c
index 0d90e8753f..80913c3b9d 100644
--- a/tests/regression/56-witness/63-hh-ex3-term.c
+++ b/tests/regression/56-witness/63-hh-ex3-term.c
@@ -19,14 +19,8 @@ int main() {
       i++;
       j++;
       __VERIFIER_assert(0 <= j);
-      __VERIFIER_assert(j <= i);
-      __VERIFIER_assert(i <= j + 3);
-      __VERIFIER_assert(j <= 4);
     }
     __VERIFIER_assert(0 <= j);
-    __VERIFIER_assert(j <= i);
-    __VERIFIER_assert(i <= j + 3);
-    __VERIFIER_assert(j <= 4);
     i = i - j + 1;
   }
   return 0;

From ac8baaa8b551c7e6324d7e37c3d94d6256c9f355 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 1 Aug 2023 16:26:01 +0300
Subject: [PATCH 14/55] Disable witness lifter if GraphML witness generation
 disabled

---
 src/framework/control.ml |  2 +-
 src/witness/witness.ml   | 54 ++++++++++++++++++++++++++++++++--------
 2 files changed, 44 insertions(+), 12 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5ceddf2870..cd3a8b5f74 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = get_bool "ana.sv-comp.enabled" || get_bool "exp.arg" in
+  let arg_enabled = get_bool "witness.enabled" || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index aff9a01383..f73a2755c8 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -297,12 +297,45 @@ struct
   module ArgTool = ArgTools.Make (R)
   module NHT = ArgTool.NHT
 
+  module type BiArgInvariant =
+  sig
+    include ArgTools.BiArg
+    val find_invariant: Node.t -> Invariant.t
+  end
+
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
-    let module Arg = (val ArgTool.create entrystates) in
+    let module Arg: BiArgInvariant =
+      (val if GobConfig.get_bool "witness.enabled" then (
+          let module Arg = (val ArgTool.create entrystates) in
+          let module Arg =
+          struct
+            include Arg
 
-    let find_invariant (n, c, i) =
-      let context = {Invariant.default_context with path = Some i} in
-      ask_local (n, c) (Invariant context)
+            let find_invariant (n, c, i) =
+              let context = {Invariant.default_context with path = Some i} in
+              ask_local (n, c) (Invariant context)
+          end
+          in
+          (module Arg: BiArgInvariant)
+        )
+        else (
+          let module Arg =
+          struct
+            module Node = ArgTool.Node
+            module Edge = MyARG.InlineEdge
+            let next _ = []
+            let prev _ = []
+            let find_invariant _ = Invariant.none
+            let main_entry =
+              let lvar = WitnessUtil.find_main_entry entrystates in
+              (fst lvar, snd lvar, -1)
+            let iter_nodes f = f main_entry
+            let query _ q = Queries.Result.top q
+          end
+          in
+          (module Arg: BiArgInvariant)
+        )
+      )
     in
 
     match Task.specification with
@@ -324,7 +357,7 @@ struct
         struct
           module Arg = Arg
           let result = Result.True
-          let invariant = find_invariant
+          let invariant = Arg.find_invariant
           let is_violation _ = false
           let is_sink _ = false
         end
@@ -332,13 +365,13 @@ struct
         (module TaskResult:WitnessTaskResult)
       ) else (
         let is_violation = function
-          | FunctionEntry f, _, _ when Svcomp.is_error_function f.svar -> true
-          | _, _, _ -> false
+          | FunctionEntry f when Svcomp.is_error_function f.svar -> true
+          | _ -> false
         in
         (* redefine is_violation to shift violations back by one, so enterFunction __VERIFIER_error is never used *)
         let is_violation n =
           Arg.next n
-          |> List.exists (fun (_, to_n) -> is_violation to_n)
+          |> List.exists (fun (_, to_n) -> is_violation (Arg.Node.cfgnode to_n))
         in
         let violations =
           (* TODO: fold_nodes?s *)
@@ -363,7 +396,7 @@ struct
           struct
             module Arg = Arg
             let result = Result.Unknown
-            let invariant = find_invariant
+            let invariant = Arg.find_invariant
             let is_violation = is_violation
             let is_sink = is_sink
           end
@@ -454,7 +487,7 @@ struct
         struct
           module Arg = Arg
           let result = Result.True
-          let invariant = find_invariant
+          let invariant = Arg.find_invariant
           let is_violation _ = false
           let is_sink _ = false
         end
@@ -480,7 +513,6 @@ struct
 
     print_task_result (module TaskResult);
 
-    (* TODO: use witness.enabled elsewhere as well *)
     if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then (
       let witness_path = get_string "witness.path" in
       Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult)

From 33eb6748eaa0f0b36e8fbc24744caf9f4cb3be86 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 1 Aug 2023 17:01:46 +0300
Subject: [PATCH 15/55] Enable witness.invariant.other in svcomp-yaml-validate
 conf

---
 conf/svcomp-yaml-validate.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
index 05bb1ebcc2..fc2ada7143 100644
--- a/conf/svcomp-yaml-validate.json
+++ b/conf/svcomp-yaml-validate.json
@@ -79,7 +79,7 @@
     "invariant": {
       "loop-head": true,
       "after-lock": false,
-      "other": false
+      "other": true
     }
   },
   "solver": "td3",

From 9127dadece4657c60ed81e3e9b78cd6ba98c986f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Aug 2023 10:22:39 +0300
Subject: [PATCH 16/55] Fix ARG enabled without ana.sv-comp.enabled

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

diff --git a/src/framework/control.ml b/src/framework/control.ml
index cd3a8b5f74..5cefc1a7de 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = get_bool "witness.enabled" || get_bool "exp.arg" in
+  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.enabled") || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in

From d512cb5e46e7c6e19e6ff80c1097c5ec183af2fa Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Aug 2023 10:25:48 +0300
Subject: [PATCH 17/55] Remove pthread_mutexattr_t from is_mutex_type

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

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 9d8fcc5012..a239be7c83 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -115,7 +115,7 @@ struct
     | _ -> false
 
   let is_mutex_type (t: typ): bool = match t with
-    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t" || info.tname = "pthread_mutexattr_t"
+    | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t"
     | TInt (IInt, attr) -> hasAttribute "mutex" attr
     | _ -> false
 

From 66204e417e23b40281c0b9973a94b62e653f2baf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 2 Feb 2023 14:05:38 +0200
Subject: [PATCH 18/55] Special case calloc with count 1 in base

---
 src/analyses/base.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 5b7a16e002..86c7cc5c2c 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2277,10 +2277,18 @@ struct
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
           let ik = Cilfacade.ptrdiff_ikind () in
-          let blobsize = ID.mul (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st size) (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st n) in
-          (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
+          let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
+          if ID.to_int countval = Some Z.one then (
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
+          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))]
+          )
+          else (
+            let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
+            (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
+                                                          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          )
         | _ -> st
       end
     | Realloc { ptr = p; size }, _ ->

From 22f6061df7d2c7bd3584c000389b9f0a7abf010e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Aug 2023 12:10:29 +0300
Subject: [PATCH 19/55] Fix trace-not-in-tracing semgrep rule for conjunctions

---
 .semgrep/tracing.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml
index 4892066c76..061b3efa0d 100644
--- a/.semgrep/tracing.yml
+++ b/.semgrep/tracing.yml
@@ -9,6 +9,7 @@ rules:
         - pattern: Messages.traceu
         - pattern: Messages.traceli
       - pattern-not-inside: if Messages.tracing then ...
+      - pattern-not-inside: if Messages.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING

From 870a9b847fc4d786752a49353eeb322d7babd319 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 3 Aug 2023 11:20:37 +0300
Subject: [PATCH 20/55] Fix PartitionDomain.SetSet.pretty_diff crash

---
 src/domains/partitionDomain.ml | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/src/domains/partitionDomain.ml b/src/domains/partitionDomain.ml
index eab15e1b05..9675e9bfce 100644
--- a/src/domains/partitionDomain.ml
+++ b/src/domains/partitionDomain.ml
@@ -115,18 +115,23 @@ struct
       for_all (fun p -> exists (B.leq p) y) x
 
   let pretty_diff () (y, x) =
-    (* based on DisjointDomain.PairwiseSet *)
-    let x_not_leq = filter (fun p ->
-        not (exists (fun q -> B.leq p q) y)
-      ) x
-    in
-    let p_not_leq = choose x_not_leq in
-    GoblintCil.Pretty.(
-      dprintf "%a:\n" B.pretty p_not_leq
-      ++
-      fold (fun q acc ->
-          dprintf "not leq %a because %a\n" B.pretty q B.pretty_diff (p_not_leq, q) ++ acc
-        ) y nil
+    if E.is_top x then (
+      GoblintCil.Pretty.(dprintf "%a not leq bot" pretty y)
+    )
+    else (
+      (* based on DisjointDomain.PairwiseSet *)
+      let x_not_leq = filter (fun p ->
+          not (exists (fun q -> B.leq p q) y)
+        ) x
+      in
+      let p_not_leq = choose x_not_leq in
+      GoblintCil.Pretty.(
+        dprintf "%a:\n" B.pretty p_not_leq
+        ++
+        fold (fun q acc ->
+            dprintf "not leq %a because %a\n" B.pretty q B.pretty_diff (p_not_leq, q) ++ acc
+          ) y nil
+      )
     )
 
   let meet xs ys = if is_bot xs || is_bot ys then bot () else

From 4fcfc715135d4721a156b0f9432ac0c1105142ae Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 3 Aug 2023 14:56:51 +0300
Subject: [PATCH 21/55] Add failing fixpoint test case for #1126

---
 .../73-strings/04-smtprc_strlen_fp.c          | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 tests/regression/73-strings/04-smtprc_strlen_fp.c

diff --git a/tests/regression/73-strings/04-smtprc_strlen_fp.c b/tests/regression/73-strings/04-smtprc_strlen_fp.c
new file mode 100644
index 0000000000..a046eac238
--- /dev/null
+++ b/tests/regression/73-strings/04-smtprc_strlen_fp.c
@@ -0,0 +1,21 @@
+// FIXPOINT extracted from smtprc_comb
+#include <unistd.h> // for optarg
+
+typedef unsigned int size_t; // size_t from 32bit cilly
+extern size_t strlen(char const   *__s );
+
+void *s_malloc(unsigned long size)
+{
+  void *mymem;
+  mymem = malloc((unsigned int) size);
+  return mymem;
+}
+
+int main() {
+  char const *p;
+  size_t s;
+  p = optarg;
+  s = strlen(optarg);
+  s_malloc((unsigned long) ((s + 1U) * sizeof(char)));
+  return 0;
+}

From 409cbd1f622a387f558b95f54db6cc57909f9f42 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 3 Aug 2023 14:57:43 +0300
Subject: [PATCH 22/55] Fix fixpoint issue from #1126

---
 src/analyses/base.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 86c7cc5c2c..0c5805c72c 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1055,7 +1055,6 @@ struct
            else if AD.may_be_null adr
            then M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer");
           AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
-        | Bot -> AD.bot ()
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
           AD.unknown_ptr

From ddecc8524347a0769ae425bb8738518f5b76025b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 3 Aug 2023 15:49:17 +0300
Subject: [PATCH 23/55] Move options from unassume bench to yaml confs

---
 conf/bench-yaml-validate.json  |  8 --------
 conf/bench-yaml.json           | 14 --------------
 conf/svcomp-yaml-validate.json | 13 +++++--------
 conf/svcomp-yaml.json          | 10 +++++++++-
 4 files changed, 14 insertions(+), 31 deletions(-)

diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
index ca830be08a..7b18371bd1 100644
--- a/conf/bench-yaml-validate.json
+++ b/conf/bench-yaml-validate.json
@@ -52,14 +52,6 @@
       "tokens": true
     }
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": true,
-      "other": false
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
index a24035fc9b..fd97b2c08c 100644
--- a/conf/bench-yaml.json
+++ b/conf/bench-yaml.json
@@ -48,20 +48,6 @@
       ]
     }
   },
-  "witness": {
-    "enabled": false,
-    "yaml": {
-      "enabled": true
-    },
-    "invariant": {
-      "exact": false,
-      "exclude-vars": [
-        "tmp\\(___[0-9]+\\)?",
-        "cond",
-        "RETURN"
-      ]
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {
diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
index fc2ada7143..1934a56932 100644
--- a/conf/svcomp-yaml-validate.json
+++ b/conf/svcomp-yaml-validate.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -31,6 +35,7 @@
       "region",
       "thread",
       "threadJoins",
+      "apron",
       "unassume"
     ],
     "context": {
@@ -74,14 +79,6 @@
   "exp": {
     "region-offsets": true
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": false,
-      "other": true
-    }
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
index 6e3d0e4767..e09d1c80d7 100644
--- a/conf/svcomp-yaml.json
+++ b/conf/svcomp-yaml.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -30,7 +34,8 @@
       "symb_locks",
       "region",
       "thread",
-      "threadJoins"
+      "threadJoins",
+      "apron"
     ],
     "context": {
       "widen": false
@@ -76,6 +81,9 @@
       "enabled": true
     },
     "invariant": {
+      "loop-head": true,
+      "other": false,
+      "accessed": false,
       "exact": false,
       "exclude-vars": [
         "tmp\\(___[0-9]+\\)?",

From c72fdedf8bc2281375c6c3c287e7423ef7699b1f Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 3 Aug 2023 16:12:39 +0200
Subject: [PATCH 24/55] Add MemoryLeak undefined behavior category

---
 src/util/messageCategory.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index 5452225c26..d1c8f0db3c 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -13,6 +13,7 @@ type undefined_behavior =
   | UseAfterFree
   | DoubleFree
   | InvalidMemoryDeallocation
+  | MemoryLeak
   | Uninitialized
   | DoubleLocking
   | Other
@@ -67,6 +68,7 @@ struct
     let use_after_free: category = create @@ UseAfterFree
     let double_free: category = create @@ DoubleFree
     let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation
+    let memory_leak: category = create @@ MemoryLeak
     let uninitialized: category = create @@ Uninitialized
     let double_locking: category = create @@ DoubleLocking
     let other: category = create @@ Other
@@ -117,6 +119,7 @@ struct
       | UseAfterFree -> ["UseAfterFree"]
       | DoubleFree -> ["DoubleFree"]
       | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"]
+      | MemoryLeak -> ["MemoryLeak"]
       | Uninitialized -> ["Uninitialized"]
       | DoubleLocking -> ["DoubleLocking"]
       | Other -> ["Other"]
@@ -228,6 +231,7 @@ let behaviorName = function
     |UseAfterFree -> "UseAfterFree"
     |DoubleFree -> "DoubleFree"
     |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation"
+    |MemoryLeak -> "MemoryLeak"
     |Uninitialized -> "Uninitialized"
     |DoubleLocking -> "DoubleLocking"
     |Other -> "Other"

From 9cea9fb688b9b7aad13c68f455d6e0167689e93c Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 3 Aug 2023 16:15:25 +0200
Subject: [PATCH 25/55] Add first version of a simple memory leak analysis

---
 src/analyses/memLeak.ml | 87 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 src/analyses/memLeak.ml

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
new file mode 100644
index 0000000000..d4a1bc967d
--- /dev/null
+++ b/src/analyses/memLeak.ml
@@ -0,0 +1,87 @@
+(** An analysis for the detection of memory leaks ([memLeak]). *)
+
+open GoblintCil
+open Analyses
+open MessageCategory
+
+module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
+
+module Spec : Analyses.MCPSpec =
+struct
+  include Analyses.DefaultSpec
+
+  let name () = "memLeak"
+
+  module D = ToppedVarInfoSet
+  module C = Lattice.Unit
+
+  let context _ _ = ()
+
+  (* HELPER FUNCTIONS *)
+  let warn_for_multi_threaded ctx =
+    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program isn't running in single-threaded mode. A memory leak might occur due to multi-threading"
+
+  (* TRANSFER FUNCTIONS *)
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    ctx.local
+
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    ctx.local
+
+  let body ctx (f:fundec) : D.t =
+    ctx.local
+
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    let state = ctx.local in
+    (* TODO: Is this too hacky of a solution? *)
+    if f.svar.vname = "main" && not @@ D.is_empty state then
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak from function \"%s\": %a\n" f.svar.vname D.pretty state;
+    state
+
+  let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [ctx.local, ctx.local]
+
+  let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t =
+    callee_local
+
+  let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
+    ctx.local
+
+  let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let state = ctx.local in
+    let desc = LibraryFunctions.find f in
+    match desc.special arglist with
+    | Malloc _
+    | Calloc _
+    | Realloc _ ->
+      (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *)
+      warn_for_multi_threaded ctx;
+      begin match ctx.ask Queries.HeapVar with
+        | `Lifted var -> D.add var state
+        | _ -> state
+      end
+    | Free ptr ->
+      begin match ctx.ask (Queries.MayPointTo ptr) with
+        | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
+          (* TODO: Need to always set "ana.malloc.unique_address_count" to smth > 0 *)
+          let unique_pointed_to_heap_vars =
+            Queries.LS.filter (fun (v, _) -> ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v)) a
+            |> Queries.LS.elements
+            |> List.map fst
+            |> D.of_list
+          in
+          D.diff state unique_pointed_to_heap_vars
+        | _ -> state
+      end
+    | _ -> state
+
+  let threadenter ctx lval f args = [ctx.local]
+  let threadspawn ctx lval f args fctx = ctx.local
+
+  let startstate v = D.bot ()
+  let exitstate v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file

From 3573182fa4e22ce8f448f6337b007f279c892e18 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 4 Aug 2023 10:24:36 +0200
Subject: [PATCH 26/55] Add two simple regression tests

---
 tests/regression/76-memleak/01-simple-no-mem-leak.c | 9 +++++++++
 tests/regression/76-memleak/02-simple-mem-leak.c    | 8 ++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 tests/regression/76-memleak/01-simple-no-mem-leak.c
 create mode 100644 tests/regression/76-memleak/02-simple-mem-leak.c

diff --git a/tests/regression/76-memleak/01-simple-no-mem-leak.c b/tests/regression/76-memleak/01-simple-no-mem-leak.c
new file mode 100644
index 0000000000..da6cdacddb
--- /dev/null
+++ b/tests/regression/76-memleak/01-simple-no-mem-leak.c
@@ -0,0 +1,9 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    free(p);
+
+    return 0; //NOWARN
+}
diff --git a/tests/regression/76-memleak/02-simple-mem-leak.c b/tests/regression/76-memleak/02-simple-mem-leak.c
new file mode 100644
index 0000000000..c3086433dd
--- /dev/null
+++ b/tests/regression/76-memleak/02-simple-mem-leak.c
@@ -0,0 +1,8 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    // No free => memory is leaked
+    return 0; //TODO: `make test` detects OTHER and not WARN here
+}

From ad19f893aad67e9909d1de9969ea79177f087e2e Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 16:11:15 +0200
Subject: [PATCH 27/55] Don't warn with a newline at the end

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

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index d4a1bc967d..1fc25c71ef 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -36,7 +36,7 @@ struct
     let state = ctx.local in
     (* TODO: Is this too hacky of a solution? *)
     if f.svar.vname = "main" && not @@ D.is_empty state then
-      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak from function \"%s\": %a\n" f.svar.vname D.pretty state;
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak from function \"%s\": %a" f.svar.vname D.pretty state;
     state
 
   let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =

From 3711fc4e63ca2676404c2b821eda444f6120e0f1 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 16:12:33 +0200
Subject: [PATCH 28/55] Clean up comments of 2nd memleak test case

---
 tests/regression/76-memleak/02-simple-mem-leak.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/76-memleak/02-simple-mem-leak.c b/tests/regression/76-memleak/02-simple-mem-leak.c
index c3086433dd..3673addfdf 100644
--- a/tests/regression/76-memleak/02-simple-mem-leak.c
+++ b/tests/regression/76-memleak/02-simple-mem-leak.c
@@ -4,5 +4,5 @@
 int main(int argc, char const *argv[]) {
     int *p = malloc(sizeof(int));
     // No free => memory is leaked
-    return 0; //TODO: `make test` detects OTHER and not WARN here
+    return 0; //WARN
 }

From 90d0a64f0627e0b1419d73a7e0aeff1fd9eba43c Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 16:16:23 +0200
Subject: [PATCH 29/55] Remove only definitely freed heap vars from state upon
 free()

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

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 1fc25c71ef..15a8947f15 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -63,7 +63,7 @@ struct
       end
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
-        | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
+        | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && Queries.LS.cardinal a = 1 ->
           (* TODO: Need to always set "ana.malloc.unique_address_count" to smth > 0 *)
           let unique_pointed_to_heap_vars =
             Queries.LS.filter (fun (v, _) -> ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v)) a

From 83d2578ded2cc8f228d6bd4d8d6d79cff7063430 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 18:41:08 +0200
Subject: [PATCH 30/55] Handle abort and assert special functions

Make more elaborate warning for mem leaks
---
 src/analyses/memLeak.ml | 36 +++++++++++++++++++++++++++++++-----
 1 file changed, 31 insertions(+), 5 deletions(-)

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 15a8947f15..c7a7b97843 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -22,6 +22,14 @@ struct
     if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
       M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program isn't running in single-threaded mode. A memory leak might occur due to multi-threading"
 
+  let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx =
+    let state = ctx.local in
+    if not @@ D.is_empty state then
+      if assert_exp_imprecise && Option.is_some exp then
+        M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp (Option.get exp) D.pretty state
+      else
+        M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
+
   (* TRANSFER FUNCTIONS *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     ctx.local
@@ -33,11 +41,9 @@ struct
     ctx.local
 
   let return ctx (exp:exp option) (f:fundec) : D.t =
-    let state = ctx.local in
-    (* TODO: Is this too hacky of a solution? *)
-    if f.svar.vname = "main" && not @@ D.is_empty state then
-      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak from function \"%s\": %a" f.svar.vname D.pretty state;
-    state
+    (* Returning from "main" is one possible program exit => need to check for memory leaks *)
+    if f.svar.vname = "main" then check_for_mem_leak ctx;
+    ctx.local
 
   let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, ctx.local]
@@ -74,6 +80,26 @@ struct
           D.diff state unique_pointed_to_heap_vars
         | _ -> state
       end
+    | Abort ->
+      (* An "Abort" special function indicates program exit => need to check for memory leaks *)
+      check_for_mem_leak ctx;
+      state
+    | Assert { exp; _ } ->
+      let warn_for_assert_exp =
+        match ctx.ask (Queries.EvalInt exp) with
+        | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
+        | a ->
+          begin match Queries.ID.to_bool a with
+            | Some b ->
+              (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
+              if b = false then
+                check_for_mem_leak ctx
+              else ()
+            | None -> check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp)
+          end
+      in
+      warn_for_assert_exp;
+      state
     | _ -> state
 
   let threadenter ctx lval f args = [ctx.local]

From 79d13cd3e1f5a24026f3ee9ac45239c493f330d6 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 18:41:41 +0200
Subject: [PATCH 31/55] Add further regression test cases

---
 tests/regression/76-memleak/03-simple-exit-mem-leak.c  |  7 +++++++
 tests/regression/76-memleak/04-simple-abort-mem-leak.c |  7 +++++++
 .../76-memleak/05-simple-assert-no-mem-leak.c          | 10 ++++++++++
 .../regression/76-memleak/06-simple-assert-mem-leak.c  |  8 ++++++++
 4 files changed, 32 insertions(+)
 create mode 100644 tests/regression/76-memleak/03-simple-exit-mem-leak.c
 create mode 100644 tests/regression/76-memleak/04-simple-abort-mem-leak.c
 create mode 100644 tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
 create mode 100644 tests/regression/76-memleak/06-simple-assert-mem-leak.c

diff --git a/tests/regression/76-memleak/03-simple-exit-mem-leak.c b/tests/regression/76-memleak/03-simple-exit-mem-leak.c
new file mode 100644
index 0000000000..451dafa471
--- /dev/null
+++ b/tests/regression/76-memleak/03-simple-exit-mem-leak.c
@@ -0,0 +1,7 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    exit(0); //WARN
+}
diff --git a/tests/regression/76-memleak/04-simple-abort-mem-leak.c b/tests/regression/76-memleak/04-simple-abort-mem-leak.c
new file mode 100644
index 0000000000..d4001410de
--- /dev/null
+++ b/tests/regression/76-memleak/04-simple-abort-mem-leak.c
@@ -0,0 +1,7 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    abort(); //WARN
+}
diff --git a/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c b/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
new file mode 100644
index 0000000000..bdaf448ee8
--- /dev/null
+++ b/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
@@ -0,0 +1,10 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    assert(1); //NOWARN
+    free(p);
+    return 0; //NOWARN
+}
diff --git a/tests/regression/76-memleak/06-simple-assert-mem-leak.c b/tests/regression/76-memleak/06-simple-assert-mem-leak.c
new file mode 100644
index 0000000000..aff78ddd59
--- /dev/null
+++ b/tests/regression/76-memleak/06-simple-assert-mem-leak.c
@@ -0,0 +1,8 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    assert(0); //WARN
+}

From 3bf7d4a426a10300af6983496c20d31317325d6b Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 18:47:26 +0200
Subject: [PATCH 32/55] Fix some regression test annotations

---
 tests/regression/76-memleak/05-simple-assert-no-mem-leak.c | 2 +-
 tests/regression/76-memleak/06-simple-assert-mem-leak.c    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c b/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
index bdaf448ee8..8dbf20c433 100644
--- a/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
+++ b/tests/regression/76-memleak/05-simple-assert-no-mem-leak.c
@@ -4,7 +4,7 @@
 
 int main(int argc, char const *argv[]) {
     int *p = malloc(sizeof(int));
-    assert(1); //NOWARN
+    assert(1);
     free(p);
     return 0; //NOWARN
 }
diff --git a/tests/regression/76-memleak/06-simple-assert-mem-leak.c b/tests/regression/76-memleak/06-simple-assert-mem-leak.c
index aff78ddd59..b2f78388dc 100644
--- a/tests/regression/76-memleak/06-simple-assert-mem-leak.c
+++ b/tests/regression/76-memleak/06-simple-assert-mem-leak.c
@@ -1,4 +1,4 @@
-//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+//PARAM: --set warn.assert false --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
 #include <stdlib.h>
 #include <assert.h>
 

From 908aa591cd85ae2feb8b6d041bd6da30c3b0a073 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 8 Aug 2023 18:52:55 +0200
Subject: [PATCH 33/55] Fix the mem leak check function

---
 src/analyses/memLeak.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index c7a7b97843..559f2badb7 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -25,10 +25,9 @@ struct
   let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx =
     let state = ctx.local in
     if not @@ D.is_empty state then
-      if assert_exp_imprecise && Option.is_some exp then
-        M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp (Option.get exp) D.pretty state
-      else
-        M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
+      match assert_exp_imprecise, exp with
+      | true, Some exp -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state
+      | _ -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
 
   (* TRANSFER FUNCTIONS *)
   let assign ctx (lval:lval) (rval:exp) : D.t =

From c3c4bb1f96077c17276a4bd1ba5aec52ef7c42dd Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 9 Aug 2023 15:12:56 +0200
Subject: [PATCH 34/55] Clean up the code a bit

---
 src/analyses/memLeak.ml | 25 ++-----------------------
 1 file changed, 2 insertions(+), 23 deletions(-)

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 559f2badb7..99df5695a7 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -8,7 +8,7 @@ module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topnam
 
 module Spec : Analyses.MCPSpec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "memLeak"
 
@@ -30,29 +30,11 @@ struct
       | _ -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
 
   (* TRANSFER FUNCTIONS *)
-  let assign ctx (lval:lval) (rval:exp) : D.t =
-    ctx.local
-
-  let branch ctx (exp:exp) (tv:bool) : D.t =
-    ctx.local
-
-  let body ctx (f:fundec) : D.t =
-    ctx.local
-
   let return ctx (exp:exp option) (f:fundec) : D.t =
     (* Returning from "main" is one possible program exit => need to check for memory leaks *)
     if f.svar.vname = "main" then check_for_mem_leak ctx;
     ctx.local
 
-  let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [ctx.local, ctx.local]
-
-  let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t =
-    callee_local
-
-  let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
-    ctx.local
-
   let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
     let state = ctx.local in
     let desc = LibraryFunctions.find f in
@@ -69,7 +51,7 @@ struct
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
         | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && Queries.LS.cardinal a = 1 ->
-          (* TODO: Need to always set "ana.malloc.unique_address_count" to smth > 0 *)
+          (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
           let unique_pointed_to_heap_vars =
             Queries.LS.filter (fun (v, _) -> ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v)) a
             |> Queries.LS.elements
@@ -101,9 +83,6 @@ struct
       state
     | _ -> state
 
-  let threadenter ctx lval f args = [ctx.local]
-  let threadspawn ctx lval f args fctx = ctx.local
-
   let startstate v = D.bot ()
   let exitstate v = D.top ()
 end

From 0652ea09f4892c4f39350b50bdb596ecdac1d048 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 9 Aug 2023 16:01:11 +0200
Subject: [PATCH 35/55] Add support for quick_exit

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 447263b3ef..f4a9ac803d 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -68,6 +68,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr);
     ("abort", special [] Abort);
     ("exit", special [drop "exit_code" []] Abort);
+    ("quick_exit", special [drop "exit_code" []] Abort);
     ("ungetc", unknown [drop "c" []; drop "stream" [r; w]]);
     ("scanf", unknown ((drop "format" [r]) :: (VarArgs (drop' [w]))));
     ("fscanf", unknown ((drop "stream" [r_deep; w_deep]) :: (drop "format" [r]) :: (VarArgs (drop' [w]))));

From 755e4eef2b74107d05e1c7e5498bdc1123348ce6 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 11 Aug 2023 14:02:40 +0200
Subject: [PATCH 36/55] Add regression test for a memory leak with quick_exit()

---
 .../regression/76-memleak/07-simple-quick-exit-mem-leak.c  | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c

diff --git a/tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c b/tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c
new file mode 100644
index 0000000000..eba23385b8
--- /dev/null
+++ b/tests/regression/76-memleak/07-simple-quick-exit-mem-leak.c
@@ -0,0 +1,7 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int *p = malloc(sizeof(int));
+    quick_exit(0); //WARN
+}

From b1b710ef597878488789a726c409c99107885b38 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 14 Aug 2023 10:57:10 +0300
Subject: [PATCH 37/55] =?UTF-8?q?Add=20local=20widen/narrow=20example=20fr?=
 =?UTF-8?q?om=20A=C2=B2I=20paper?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Sarah Tilscher <66023521+stilscher@users.noreply.github.com>
---
 .../regression/34-localwn_restart/06-td-a2i.c | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/regression/34-localwn_restart/06-td-a2i.c

diff --git a/tests/regression/34-localwn_restart/06-td-a2i.c b/tests/regression/34-localwn_restart/06-td-a2i.c
new file mode 100644
index 0000000000..e1fe6b05d0
--- /dev/null
+++ b/tests/regression/34-localwn_restart/06-td-a2i.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.interval --set solver td3 --enable solvers.td3.remove-wpoint
+// Example from "The Top-Down Solver — An Exercise in A²I", Section 6.
+#include <goblint.h>
+
+int main() {
+  int i, j, x;
+  i = 0;
+  while (i < 42) {
+    j = 0;
+    while (j < 17) {
+      x = i + j;
+      j++;
+    }
+    __goblint_check(j == 17);
+    __goblint_check(i >= 0);
+    __goblint_check(i <= 41);
+    i++;
+  }
+  __goblint_check(i == 42);
+  __goblint_check(j == 17); // TODO
+  return 0;
+}

From e11c982aac5925edc348389305ce1a48efb73aa0 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 14 Aug 2023 13:53:11 +0300
Subject: [PATCH 38/55] Make sem.unknown_function.call option

---
 src/analyses/libraryFunctions.ml | 3 ++-
 src/util/options.schema.json     | 7 +++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 6495341c7a..7c31d69fb8 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -1165,7 +1165,8 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
     | Read when GobConfig.get_bool "sem.unknown_function.read.args" -> args
     | Read -> []
     | Free -> []
-    | Call -> [] (* TODO: option *)
+    | Call when get_bool "sem.unknown_function.call.args" -> args
+    | Call -> []
     | Spawn when get_bool "sem.unknown_function.spawn" -> args
     | Spawn -> []
   in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index efa1dfabb8..0e89ede0b5 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1317,6 +1317,13 @@
               "type": "boolean",
               "default": true
             },
+            "call": {
+              "title": "sem.unknown_function.call",
+              "description":
+                "Unknown function call calls reachable functions",
+              "type": "boolean",
+              "default": true
+            },
             "invalidate": {
               "title": "sem.unknown_function.invalidate",
               "type": "object",

From f150fdca489dfe76e1510c6a78ececddc0a0c60e Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 14 Aug 2023 14:37:09 +0300
Subject: [PATCH 39/55] Fix rand in libraryFunctions

---
 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 7c31d69fb8..5dc311a587 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -84,7 +84,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("getchar", unknown []);
     ("putchar", unknown [drop "ch" []]);
     ("puts", unknown [drop "s" [r]]);
-    ("rand", unknown ~attrs:[ThreadUnsafe] []);
+    ("rand", special ~attrs:[ThreadUnsafe] [] Rand);
     ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]);
     ("strspn", unknown [drop "s" [r]; drop "accept" [r]]);
     ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]);
@@ -118,7 +118,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
-    ("rand", special [] Rand);
   ]
 
 (** C POSIX library functions.

From 379a7ff53d0f330e8fe92042c6cec9b37b369ccc Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 14 Aug 2023 14:37:36 +0300
Subject: [PATCH 40/55] Fix side_access call

---
 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 c09396bdd3..970895e971 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -105,7 +105,7 @@ struct
       let g: V.t = Obj.obj g in
       begin match g with
         | `Left g' -> (* accesses *)
-          (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
+          (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *)
           let trie = G.access (ctx.global g) in
           (** Distribute access to contained fields. *)
           let rec distribute_inner offset (accs, children) ancestor_accs =
@@ -202,7 +202,7 @@ struct
       let loc = 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) ((`Type f.vtype), `NoOffset) ;
+      side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ;
     );
     ctx.local
 

From 8465e0b2eb3a72230ec3c327faa47fc969aad211 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 14 Aug 2023 14:38:05 +0300
Subject: [PATCH 41/55] Rename tests to have unique numbers

---
 .../{77-thread-unsafe_fun_rc.c => 90-thread-unsafe_fun_rc.c}      | 0
 .../{78-thread-unsafe_fun_nr.c => 91-thread-unsafe_fun_nr.c}      | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/04-mutex/{77-thread-unsafe_fun_rc.c => 90-thread-unsafe_fun_rc.c} (100%)
 rename tests/regression/04-mutex/{78-thread-unsafe_fun_nr.c => 91-thread-unsafe_fun_nr.c} (100%)

diff --git a/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c
similarity index 100%
rename from tests/regression/04-mutex/77-thread-unsafe_fun_rc.c
rename to tests/regression/04-mutex/90-thread-unsafe_fun_rc.c
diff --git a/tests/regression/04-mutex/78-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c
similarity index 100%
rename from tests/regression/04-mutex/78-thread-unsafe_fun_nr.c
rename to tests/regression/04-mutex/91-thread-unsafe_fun_nr.c

From a7656fbb3b926bc55b7e8b6afb1555caa7ceef98 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 18 Aug 2023 09:43:49 +0200
Subject: [PATCH 42/55] Add check for memory deallocation at an offset

---
 src/analyses/base.ml | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a213170ba2..2ef8257d59 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2013,14 +2013,21 @@ struct
     let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in
     invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs
 
-  let check_free_of_non_heap_mem ctx special_fn ptr =
+  let check_invalid_mem_dealloc ctx special_fn ptr =
+    let has_offset = function
+      | `NoOffset -> false
+      | `Field _
+      | `Index _ -> true
+    in
     match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
     | Address a ->
       let points_to_set = addrToLvalSet a in
       if Q.LS.is_top points_to_set then
-        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potential free of non-dynamically allocated memory may occur" d_exp ptr special_fn.vname
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname
       else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
+      else if Q.LS.exists (fun (_, o) -> has_offset o) points_to_set then
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr
     | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
 
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
@@ -2304,7 +2311,7 @@ struct
       end
     | Realloc { ptr = p; size }, _ ->
       (* Realloc shouldn't be passed non-dynamically allocated memory *)
-      check_free_of_non_heap_mem ctx f p;
+      check_invalid_mem_dealloc ctx f p;
       begin match lv with
         | Some lv ->
           let ask = Analyses.ask_of_ctx ctx in
@@ -2338,7 +2345,7 @@ struct
       end
     | Free ptr, _ ->
       (* Free shouldn't be passed non-dynamically allocated memory *)
-      check_free_of_non_heap_mem ctx f ptr;
+      check_invalid_mem_dealloc ctx f ptr;
       st
     | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
     | Setjmp { env }, _ ->

From 6ac2a6f2b0e2a149b064937369bb6d098efd7077 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 18 Aug 2023 09:46:31 +0200
Subject: [PATCH 43/55] Refactor out "has_offset" as helper function

---
 src/analyses/base.ml | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2ef8257d59..1087678c8b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -138,6 +138,11 @@ struct
   let project ask p_opt cpa fundec =
     CPA.mapi (fun varinfo value -> project_val ask (attributes_varinfo varinfo fundec) p_opt value (is_privglob varinfo)) cpa
 
+  let has_offset = function
+    | `NoOffset -> false
+    | `Field _
+    | `Index _ -> true
+
 
   (**************************************************************************
    * Initializing my variables
@@ -1262,11 +1267,6 @@ struct
         match p with
         | Address a ->
           let s = addrToLvalSet a in
-          let has_offset = function
-            | `NoOffset -> false
-            | `Field _
-            | `Index _ -> true
-          in
           (* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
           if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || has_offset o) s then
             Queries.Result.bot q
@@ -2014,11 +2014,6 @@ struct
     invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs
 
   let check_invalid_mem_dealloc ctx special_fn ptr =
-    let has_offset = function
-      | `NoOffset -> false
-      | `Field _
-      | `Index _ -> true
-    in
     match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
     | Address a ->
       let points_to_set = addrToLvalSet a in

From 0ed93f2db6901bc94e2d9ef4162d11064cf44b3f Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 18 Aug 2023 10:02:05 +0200
Subject: [PATCH 44/55] Add more regression test cases for invalid dealloc

---
 .../75-invalid_dealloc/05-free-at-offset.c        |  9 +++++++++
 .../75-invalid_dealloc/06-realloc-at-offset.c     | 11 +++++++++++
 .../75-invalid_dealloc/07-free-at-struct-offset.c | 15 +++++++++++++++
 .../08-realloc-at-struct-offset.c                 | 15 +++++++++++++++
 4 files changed, 50 insertions(+)
 create mode 100644 tests/regression/75-invalid_dealloc/05-free-at-offset.c
 create mode 100644 tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
 create mode 100644 tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
 create mode 100644 tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c

diff --git a/tests/regression/75-invalid_dealloc/05-free-at-offset.c b/tests/regression/75-invalid_dealloc/05-free-at-offset.c
new file mode 100644
index 0000000000..c9ec66c769
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/05-free-at-offset.c
@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(42 * sizeof(char));
+    ptr = ptr + 7;
+    free(ptr); //WARN
+
+    return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c b/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
new file mode 100644
index 0000000000..64a42654e1
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+#define MAX_SIZE 5000
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(42 * sizeof(char));
+    ptr = ptr + 7;
+    realloc(ptr, MAX_SIZE); //WARN
+
+    return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
new file mode 100644
index 0000000000..f5f727f280
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    char *x;
+    int y;
+} custom_t;
+
+int main(int argc, char const *argv[]) {
+    custom_t *struct_ptr = malloc(sizeof(custom_t));
+    struct_ptr->x = malloc(10 * sizeof(char));
+    free(struct_ptr->x); //NOWARN
+    free(struct_ptr->y); //WARN
+    free(struct_ptr); //NOWARN
+    return 0;
+}
diff --git a/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
new file mode 100644
index 0000000000..c163396524
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    char *x;
+    int y;
+} custom_t;
+
+int main(int argc, char const *argv[]) {
+    custom_t *struct_ptr = malloc(sizeof(custom_t));
+    struct_ptr->x = malloc(10 * sizeof(char));
+    realloc(struct_ptr->x, 50); //NOWARN
+    realloc(struct_ptr->y, 50); //WARN
+    realloc(struct_ptr, 2 * sizeof(custom_t)); //NOWARN
+    return 0;
+}

From cb811e1f6d6ff42c4f3f62f93d18c34c767fad75 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 18 Aug 2023 11:19:28 +0200
Subject: [PATCH 45/55] Replace has_offset with comparisons

---
 src/analyses/base.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 1087678c8b..558646a8e2 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -138,11 +138,6 @@ struct
   let project ask p_opt cpa fundec =
     CPA.mapi (fun varinfo value -> project_val ask (attributes_varinfo varinfo fundec) p_opt value (is_privglob varinfo)) cpa
 
-  let has_offset = function
-    | `NoOffset -> false
-    | `Field _
-    | `Index _ -> true
-
 
   (**************************************************************************
    * Initializing my variables
@@ -1268,7 +1263,7 @@ struct
         | Address a ->
           let s = addrToLvalSet a in
           (* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
-          if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || has_offset o) s then
+          if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset) s then
             Queries.Result.bot q
           else (
             let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a  None in
@@ -2021,7 +2016,7 @@ struct
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname
       else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
-      else if Q.LS.exists (fun (_, o) -> has_offset o) points_to_set then
+      else if Q.LS.exists (fun (_, o) -> o <> `NoOffset) points_to_set then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr
     | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
 

From 0e61b9edf96f6c9fbb80121d0f3b81c9bfdbdfff Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Aug 2023 12:48:34 +0300
Subject: [PATCH 46/55] Add script for finding modules missing from API
 documentation

---
 scripts/goblint-lib-modules.py | 58 ++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100755 scripts/goblint-lib-modules.py

diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
new file mode 100755
index 0000000000..0347f5dc86
--- /dev/null
+++ b/scripts/goblint-lib-modules.py
@@ -0,0 +1,58 @@
+#!/usr/bin/python3
+
+from pathlib import Path
+import re
+import sys
+
+src_root_path = Path("./src")
+
+goblint_lib_path = src_root_path / "goblint_lib.ml"
+goblint_lib_modules = set()
+
+with goblint_lib_path.open() as goblint_lib_file:
+    for line in goblint_lib_file:
+        line = line.strip()
+        m = re.match(r"module (.*) = .*", line)
+        if m is not None:
+            module_name = m.group(1)
+            goblint_lib_modules.add(module_name)
+
+src_vendor_path = src_root_path / "vendor"
+exclude_module_names = set([
+    "Goblint_lib", # itself
+
+    # executables
+    "Goblint",
+    "MessagesCompare",
+    "PrivPrecCompare",
+    "ApronPrecCompare",
+    "Mainspec",
+
+    # libraries
+    "Goblint_timing",
+    "Goblint_backtrace",
+    "Goblint_sites",
+    "Goblint_build_info",
+
+    "MessageCategory", # included in Messages
+    "PreValueDomain", # included in ValueDomain
+    "SpecCore", # spec stuff
+    "SpecUtil", # spec stuff
+])
+
+src_modules = set()
+
+for ml_path in src_root_path.glob("**/*.ml"):
+    if str(ml_path).startswith(str(src_vendor_path)):
+        continue
+
+    module_name = ml_path.with_suffix("").with_suffix("").name
+    module_name = module_name[0].upper() + module_name[1:]
+    if module_name.endswith("0") or module_name.endswith("_intf") or module_name in exclude_module_names:
+        continue
+
+    src_modules.add(module_name)
+
+if len(src_modules) > 0:
+    print(f"Modules missing from {goblint_lib_path}: {src_modules - goblint_lib_modules}")
+    sys.exit(1)

From f618594ef2e9b1644a79890cab29b46340157d9b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Aug 2023 12:52:10 +0300
Subject: [PATCH 47/55] Add missing analyses to API documentation

---
 src/analyses/tmpSpecial.ml | 7 ++++---
 src/goblint_lib.ml         | 3 +++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml
index c4af80906e..2d38972d7a 100644
--- a/src/analyses/tmpSpecial.ml
+++ b/src/analyses/tmpSpecial.ml
@@ -1,5 +1,6 @@
-(* Analysis that tracks which variables hold the results of calls to math library functions.
-   For each equivalence a set of expressions is tracked, that contains the arguments of the corresponding call as well as the Lval it is assigned to, so an equivalence can be removed if one of these expressions may be changed.*)
+(** Analysis that tracks which variables hold the results of calls to math library functions ([tmpSpecial]). *)
+
+(** For each equivalence a set of expressions is tracked, that contains the arguments of the corresponding call as well as the Lval it is assigned to, so an equivalence can be removed if one of these expressions may be changed. *)
 
 module VarEq = VarEq.Spec
 
@@ -69,7 +70,7 @@ struct
         (* actually it would be necessary to check here, if one of the arguments is written by the call. However this is not the case for any of the math functions and no other functions are covered so far *)
         if List.exists (fun arg -> VarEq.may_change ask (mkAddrOf lv) arg) arglist then
           d
-        else 
+        else
           D.add (v, Offset.Exp.of_cil offs) ((ML.lift fun_args, Deps.of_list ((Lval lv)::arglist))) d
       | _ -> d
 
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index d8d74acc0f..625e81f18b 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -74,6 +74,7 @@ module ApronAnalysis = ApronAnalysis
 module AffineEqualityAnalysis = AffineEqualityAnalysis
 module VarEq = VarEq
 module CondVars = CondVars
+module TmpSpecial = TmpSpecial
 
 (** {2 Heap}
 
@@ -82,6 +83,8 @@ module CondVars = CondVars
 module Region = Region
 module MallocFresh = MallocFresh
 module Malloc_null = Malloc_null
+module MemLeak = MemLeak
+module UseAfterFree = UseAfterFree
 
 (** {2 Concurrency}
 

From b9de7cb70349a8d6d416fffb3a7cc917166a217e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Aug 2023 12:54:15 +0300
Subject: [PATCH 48/55] Remove unused OSEK FlagModeDomain

---
 src/cdomains/flagModeDomain.ml | 52 ----------------------------------
 1 file changed, 52 deletions(-)
 delete mode 100644 src/cdomains/flagModeDomain.ml

diff --git a/src/cdomains/flagModeDomain.ml b/src/cdomains/flagModeDomain.ml
deleted file mode 100644
index 70ee6d0015..0000000000
--- a/src/cdomains/flagModeDomain.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(* TODO: unused *)
-
-module     Eq = IntDomain.MakeBooleans (struct let truename="==" let falsename="!=" end)
-module Method = IntDomain.MakeBooleans (struct let truename="guard" let falsename="assign" end)
-
-module L_names =
-struct
-  let bot_name = "unreachable"
-  let top_name = "unknown"
-end
-
-module P =
-struct
-  include Lattice.Flat (Printable.Prod3 (Method) (Eq) (IntDomain.FlatPureIntegers)) (L_names)
-  let show x = match x with
-    | `Lifted (m,b,e) -> Method.show m ^"ed "^ Eq.show b ^ " " ^ IntDomain.FlatPureIntegers.show e
-    | `Top -> top_name
-    | `Bot -> bot_name
-
-  let join x y = match x,y with
-    | `Bot , z | z , `Bot -> z
-    | `Lifted (false,_,c1),`Lifted (false,_,c2) when c1=c2 -> y
-    | `Lifted (true,false,c1),`Lifted (true,false,c2) when c1=c2 -> y
-    | `Lifted (true,true,c1),`Lifted (true, true, c2) when c1=c2 -> y
-    | `Lifted (true,true,c1),`Lifted (true, false, c2) when not(c1=c2) -> y
-    | `Lifted (true,false,c1),`Lifted (true, true, c2) when not(c1=c2) -> x
-    | _ -> `Top
-
-
-  let leq (x:t) (y:t) = match x,y with
-    | `Bot , _  -> true
-    | _ , `Top -> true
-    | _, `Bot -> false
-    | `Top ,_ -> false
-    | `Lifted (false,_,c1), `Lifted (false,_,c2) -> c1=c2
-    | _, `Lifted (false,_,_) ->  false
-    | `Lifted (false,_,_), _ ->  true
-    | `Lifted (true,true,c1),`Lifted (true, true, c2)  -> c1=c2
-    | _, `Lifted (true,true,_) -> false
-    | `Lifted (true, true, _), _ -> true
-    | `Lifted (true,false,c1),`Lifted (true,false,c2) -> c1=c2
-    (*    | _, `Lifted (true,false,c1) -> false
-          | `Lifted (true,false,_), _ -> true    *)
-    (*     | _ -> false *)
-end
-
-module Dom =
-struct
-  include MapDomain.MapTop_LiftBot (Basetype.Variables) (P)
-
-  (*   let find k x = if mem k x then find k x else P.top() *)
-end

From 67dcdfd73d30797884d29f55832f609d8c1986bc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Aug 2023 12:54:25 +0300
Subject: [PATCH 49/55] Fix goblint-lib-modules.py exit code

---
 scripts/goblint-lib-modules.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index 0347f5dc86..342f9a76bd 100755
--- a/scripts/goblint-lib-modules.py
+++ b/scripts/goblint-lib-modules.py
@@ -53,6 +53,7 @@
 
     src_modules.add(module_name)
 
-if len(src_modules) > 0:
-    print(f"Modules missing from {goblint_lib_path}: {src_modules - goblint_lib_modules}")
+missing_modules = src_modules - goblint_lib_modules
+if len(missing_modules) > 0:
+    print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
     sys.exit(1)

From a135dea1f9a0146893f1b38458f3839d8a75f8f6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Aug 2023 12:55:45 +0300
Subject: [PATCH 50/55] Add goblint-lib-modules.py to docs workflow

---
 .github/workflows/docs.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index cd0414d6fe..aa69baf958 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -32,6 +32,9 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v3
 
+      - name: Check for undocumented modules
+        run: python scripts/goblint-lib-modules.py
+
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
           # otherwise setup-ocaml pins non-locked dependencies

From 8614b522db13b1586bbe0f6ad0d162d07695e13d Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 18 Aug 2023 12:01:24 +0200
Subject: [PATCH 51/55] Fix two test cases by taking addresses of struct fields

---
 .../regression/75-invalid_dealloc/07-free-at-struct-offset.c  | 4 ++--
 .../75-invalid_dealloc/08-realloc-at-struct-offset.c          | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
index f5f727f280..f64d66d8fc 100644
--- a/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
+++ b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
@@ -8,8 +8,8 @@ typedef struct custom_t {
 int main(int argc, char const *argv[]) {
     custom_t *struct_ptr = malloc(sizeof(custom_t));
     struct_ptr->x = malloc(10 * sizeof(char));
-    free(struct_ptr->x); //NOWARN
-    free(struct_ptr->y); //WARN
+    free(&struct_ptr->x); //NOWARN
+    free(&struct_ptr->y); //WARN
     free(struct_ptr); //NOWARN
     return 0;
 }
diff --git a/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
index c163396524..fddb8a7694 100644
--- a/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
+++ b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
@@ -8,8 +8,8 @@ typedef struct custom_t {
 int main(int argc, char const *argv[]) {
     custom_t *struct_ptr = malloc(sizeof(custom_t));
     struct_ptr->x = malloc(10 * sizeof(char));
-    realloc(struct_ptr->x, 50); //NOWARN
-    realloc(struct_ptr->y, 50); //WARN
+    realloc(&struct_ptr->x, 50); //NOWARN
+    realloc(&struct_ptr->y, 50); //WARN
     realloc(struct_ptr, 2 * sizeof(custom_t)); //NOWARN
     return 0;
 }

From 92c0dcae14badbb2be23a62d7c5e15951f877bc2 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 18 Aug 2023 12:01:45 +0200
Subject: [PATCH 52/55] Use cmp_zero_offset for checking invalid free at offset

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 558646a8e2..824fde18d9 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2016,7 +2016,7 @@ struct
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname
       else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
-      else if Q.LS.exists (fun (_, o) -> o <> `NoOffset) points_to_set then
+      else if Q.LS.exists (fun (_, o) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr
     | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
 

From b55afa6a6fdafab6f9a9b3c4502d3d2e2d15e9d9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 1 Sep 2023 13:05:30 +0300
Subject: [PATCH 53/55] Fix semgrep 1.38 compatibility

---
 .github/workflows/semgrep.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml
index acd696e597..b46713d510 100644
--- a/.github/workflows/semgrep.yml
+++ b/.github/workflows/semgrep.yml
@@ -19,7 +19,7 @@ jobs:
         uses: actions/checkout@v3
 
       - name: Run semgrep
-        run: semgrep scan --sarif --output=semgrep.sarif
+        run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
         uses: github/codeql-action/upload-sarif@v2

From fc67853d42ce48745443adc9768e3d4fe14f76d5 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Mon, 4 Sep 2023 20:41:25 +0000
Subject: [PATCH 54/55] Bump actions/checkout from 3 to 4

Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to 4.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v3...v4)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
---
 .github/workflows/coverage.yml    | 2 +-
 .github/workflows/docker.yml      | 2 +-
 .github/workflows/docs.yml        | 2 +-
 .github/workflows/indentation.yml | 2 +-
 .github/workflows/locked.yml      | 6 +++---
 .github/workflows/metadata.yml    | 4 ++--
 .github/workflows/options.yml     | 2 +-
 .github/workflows/semgrep.yml     | 2 +-
 .github/workflows/unlocked.yml    | 8 ++++----
 9 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index 7472cbc820..5635ebbeea 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -28,7 +28,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 02c5f07d90..1ef104db29 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -35,7 +35,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index aa69baf958..e1648904c3 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Check for undocumented modules
         run: python scripts/goblint-lib-modules.py
diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
index 14db288d60..e22e674301 100644
--- a/.github/workflows/indentation.yml
+++ b/.github/workflows/indentation.yml
@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 358682a2f3..007ea34619 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -101,7 +101,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -141,7 +141,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
index da20c6b675..1092606bc6 100644
--- a/.github/workflows/metadata.yml
+++ b/.github/workflows/metadata.yml
@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
@@ -36,7 +36,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3
diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
index b8522c03bb..b5f690a700 100644
--- a/.github/workflows/options.yml
+++ b/.github/workflows/options.yml
@@ -15,7 +15,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3
diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml
index b46713d510..bd2dfd285c 100644
--- a/.github/workflows/semgrep.yml
+++ b/.github/workflows/semgrep.yml
@@ -16,7 +16,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run semgrep
         run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 2bec6b72fb..15cd9138d8 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -45,7 +45,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -131,7 +131,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -208,7 +208,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
         uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
@@ -246,7 +246,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2

From d97504bf08c8f79e04539665432ad05ffd843523 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 7 Sep 2023 16:13:29 +0300
Subject: [PATCH 55/55] Fix YAML witness unassume indentation (PR #1124)

---
 src/analyses/base.ml   |  6 +++--
 src/witness/witness.ml | 58 +++++++++++++++++++++---------------------
 2 files changed, 33 insertions(+), 31 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4a49b9eed0..b74555b7ad 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2297,8 +2297,10 @@ struct
           let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
           let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
           if ID.to_int countval = Some Z.one then (
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
-          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))]
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+              add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false);
+              eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))
+            ]
           )
           else (
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index f73a2755c8..baa465a1b3 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -306,35 +306,35 @@ struct
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
       (val if GobConfig.get_bool "witness.enabled" then (
-          let module Arg = (val ArgTool.create entrystates) in
-          let module Arg =
-          struct
-            include Arg
-
-            let find_invariant (n, c, i) =
-              let context = {Invariant.default_context with path = Some i} in
-              ask_local (n, c) (Invariant context)
-          end
-          in
-          (module Arg: BiArgInvariant)
-        )
-        else (
-          let module Arg =
-          struct
-            module Node = ArgTool.Node
-            module Edge = MyARG.InlineEdge
-            let next _ = []
-            let prev _ = []
-            let find_invariant _ = Invariant.none
-            let main_entry =
-              let lvar = WitnessUtil.find_main_entry entrystates in
-              (fst lvar, snd lvar, -1)
-            let iter_nodes f = f main_entry
-            let query _ q = Queries.Result.top q
-          end
-          in
-          (module Arg: BiArgInvariant)
-        )
+           let module Arg = (val ArgTool.create entrystates) in
+           let module Arg =
+           struct
+             include Arg
+
+             let find_invariant (n, c, i) =
+               let context = {Invariant.default_context with path = Some i} in
+               ask_local (n, c) (Invariant context)
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+         else (
+           let module Arg =
+           struct
+             module Node = ArgTool.Node
+             module Edge = MyARG.InlineEdge
+             let next _ = []
+             let prev _ = []
+             let find_invariant _ = Invariant.none
+             let main_entry =
+               let lvar = WitnessUtil.find_main_entry entrystates in
+               (fst lvar, snd lvar, -1)
+             let iter_nodes f = f main_entry
+             let query _ q = Queries.Result.top q
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
       )
     in