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 01/56] 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 02/56] 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 03/56] 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 04/56] 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 05/56] 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 06/56] 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 07/56] 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 08/56] 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 09/56] 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 10/56] 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 11/56] 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 12/56] 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 13/56] 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 14/56] 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 15/56] 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 16/56] 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 17/56] 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 18/56] 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 19/56] 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 20/56] 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 21/56] 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 22/56] 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 23/56] 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 24/56] 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 25/56] 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 26/56] 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 27/56] 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 28/56] 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 29/56] 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 30/56] 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 31/56] 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 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 32/56] 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 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 33/56] 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 34/56] 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 35/56] 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 36/56] 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 37/56] 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 38/56] 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 39/56] 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 40/56] 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 41/56] 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 42/56] 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 43/56] 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 fe1660e0e74d6934aec68d590ade46d29b171d0c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Aug 2023 10:24:32 +0300
Subject: [PATCH 44/56] Remove RaceAnalysis joke

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

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index f617df2048..462834e2f4 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -3,7 +3,7 @@
 open GoblintCil
 open Analyses
 
-(** Data race analysis with tries and hookers.
+(** Data race analysis with tries for offsets and type-based memory locations for open code.
 
     Accesses are to memory locations ({{!Access.Memo} memos}) which consist of a root and offset.
     {{!Access.MemoRoot} Root} can be:

From 00fb4964810643a998fb522cfc4e470b07a21ec8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Aug 2023 10:30:09 +0300
Subject: [PATCH 45/56] Add C declarations to race analysis documentation

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

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 462834e2f4..d452b6b131 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -41,7 +41,20 @@ open Analyses
     This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets.
     It ensures that corresponding trie nodes exist for traversal later. *)
 
-(** Example structure of related memos for race checking:
+(** Given C declarations:
+    {@c[
+    struct S {
+      int f;
+    };
+
+    struct T {
+      struct S s;
+    };
+
+    struct T t;
+    ]}
+
+    Example structure of related memos for race checking:
     {v
      (int)   (S)     (T)
         \   /   \   /   \
@@ -54,9 +67,7 @@ open Analyses
     where:
     - [(int)] is a type-based memo root for the primitive [int] type;
     - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots;
-    - [f] is a field of [S] and [s] is a field of [T];
-    - [t] is a global variable of type [T].
-    - prefix relations are indicated by [/];
+    - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left;
     - type suffix relations are indicated by [\ ].
 
     Prefix races:

From 0329b30ad74cce93b55d4998f169faf108ec3eca Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Aug 2023 10:44:05 +0300
Subject: [PATCH 46/56] Make race analysis documentation example races list
 complete

---
 src/analyses/raceAnalysis.ml | 46 ++++++++++++++++++++++++++++++------
 1 file changed, 39 insertions(+), 7 deletions(-)

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index d452b6b131..4ca1094b4a 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -70,28 +70,60 @@ open Analyses
     - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left;
     - type suffix relations are indicated by [\ ].
 
-    Prefix races:
+    All same-node races:
+    - Race between [t.s.f] and [t.s.f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [t.s] is checked/reported at [t.s].
+    - Race between [t] and [t] is checked/reported at [t].
+    - Race between [(T).s.f] and [(T).s.f] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(T).s] is checked/reported at [(T).s].
+    - Race between [(T)] and [(T)] is checked/reported at [(T)].
+    - Race between [(S).f] and [(S).f] is checked/reported at [(S).f].
+    - Race between [(S)] and [(S)] is checked/reported at [(S)].
+    - Race between [(int)] and [(int)] is checked/reported at [(int)].
+
+    All prefix races:
     - Race between [t.s.f] and [t.s] is checked/reported at [t.s.f].
     - Race between [t.s.f] and [t] is checked/reported at [t.s.f].
     - Race between [t.s] and [t] is checked/reported at [t.s].
-    - Race between [t] and [t] is checked/reported at [t].
+    - Race between [(T).s.f] and [(T).s] is checked/reported at [(T).s.f].
+    - Race between [(T).s.f] and [(T)] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(T)] is checked/reported at [(T).s].
     - Race between [(S).f] and [(S)] is checked/reported at [(S).f].
 
-    Type suffix races:
+    All type suffix races:
     - Race between [t.s.f] and [(T).s.f] is checked/reported at [t.s.f].
     - Race between [t.s.f] and [(S).f] is checked/reported at [t.s.f].
     - Race between [t.s.f] and [(int)] is checked/reported at [t.s.f].
+    - Race between [(T).s.f] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T).s.f] and [(int)] is checked/reported at [(T).s.f].
     - Race between [(S).f] and [(int)] is checked/reported at [(S).f].
+    - Race between [t.s] and [(T).s] is checked/reported at [t.s].
+    - Race between [t.s] and [(S)] is checked/reported at [t.s].
+    - Race between [(T).s] and [(S)] is checked/reported at [(T).s].
+    - Race between [t] and [(T)] is checked/reported at [t].
 
-    Type suffix prefix races:
+    All type suffix prefix races:
     - Race between [t.s.f] and [(T).s] is checked/reported at [t.s.f].
     - Race between [t.s.f] and [(T)] is checked/reported at [t.s.f].
     - Race between [t.s.f] and [(S)] is checked/reported at [t.s.f].
     - Race between [(T).s.f] and [(S)] is checked/reported at [(T).s.f].
-
-    Prefix-type suffix races:
+    - Race between [t.s] and [(T)] is checked/reported at [t.s].
+
+    All prefix-type suffix races:
+    - Race between [t.s] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [(int)] is checked/reported at [t.s.f].
+    - Race between [t] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t] and [(int)] is checked/reported at [t.s.f].
+    - Race between [t] and [(T).s] is checked/reported at [t.s].
+    - Race between [t] and [(S)] is checked/reported at [t.s].
     - Race between [(T).s] and [(S).f] is checked/reported at [(T).s.f].
-    - Race between [t] and [(S).f] is checked/reported at [t.s.f]. *)
+    - Race between [(T).s] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(S)] is checked/reported at [(T).s].
+    - Race between [(S)] and [(int)] is checked/reported at [(S).f]. *)
 
 
 (** Data race analyzer without base --- this is the new standard *)

From a8a8899d94f237cb76825b8a78f508fa50d3f450 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Aug 2023 17:43:25 +0300
Subject: [PATCH 47/56] Add TODO for ana.race.direct-arithmetic in lazy outer
 distribution

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

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 4ca1094b4a..d6621154b7 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -241,6 +241,7 @@ struct
     match root, offset with
     | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *)
     | _, `NoOffset -> None (* primitive type *)
+    (* TODO: should handle ana.race.direct-arithmetic special case here? *)
     | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *)
     | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *)
     | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)

From 4e1cf15f28143ec2e231e791f38f75e25ebd8efe Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Aug 2023 15:10:16 +0300
Subject: [PATCH 48/56] Add comment about ana.race.direct-arithmetic

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

diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index d6621154b7..74a98af6be 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -238,10 +238,11 @@ struct
 
   (** Get immediate type_suffix memo. *)
   let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option =
+    (* No need to make ana.race.direct-arithmetic return None here,
+       because (int) is empty anyway since Access.add_distribute_outer isn't called. *)
     match root, offset with
     | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *)
     | _, `NoOffset -> None (* primitive type *)
-    (* TODO: should handle ana.race.direct-arithmetic special case here? *)
     | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *)
     | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *)
     | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)

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 49/56] 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 50/56] 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 51/56] 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
 

From d3ec6172b6f9f8060e0dadcbee439f4b29d00a9b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 11 Sep 2023 11:49:16 +0300
Subject: [PATCH 52/56] Add missing thread-unsafe functions to LibraryFunctions
 (closes #723)

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 5dc311a587..c4378f6e14 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -111,7 +111,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("difftime", unknown [drop "time1" []; drop "time2" []]);
     ("system", unknown ~attrs:[ThreadUnsafe] [drop "command" [r]]);
     ("wcscat", unknown [drop "dest" [r; w]; drop "src" [r]]);
+    ("wctomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]; drop "wc" []]);
     ("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]; drop "wc" []; drop "ps" [r_deep; w_deep]]);
+    ("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]);
+    ("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]);
     ("abs", unknown [drop "j" []]);
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
@@ -142,9 +145,11 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("dlerror", unknown ~attrs:[ThreadUnsafe] []);
     ("drand48", unknown ~attrs:[ThreadUnsafe] []);
     ("encrypt", unknown ~attrs:[ThreadUnsafe] [drop "block" [r; w]; drop "edflag" []]);
+    ("setkey", unknown ~attrs:[ThreadUnsafe] [drop "key" [r]]);
     ("endgrent", unknown ~attrs:[ThreadUnsafe] []);
     ("endpwent", unknown ~attrs:[ThreadUnsafe] []);
     ("fcvt", unknown ~attrs:[ThreadUnsafe] [drop "number" []; drop "ndigits" []; drop "decpt" [w]; drop "sign" [w]]);
+    ("ecvt", unknown ~attrs:[ThreadUnsafe] [drop "number" []; drop "ndigits" []; drop "decpt" [w]; drop "sign" [w]]);
     ("gcvt", unknown ~attrs:[ThreadUnsafe] [drop "number" []; drop "ndigit" []; drop "buf" [w]]);
     ("getdate", unknown ~attrs:[ThreadUnsafe] [drop "string" [r]]);
     ("getenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]);
@@ -279,6 +284,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); (* has two underscores *)
     ("sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env });
     ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
+    ("ftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []]); (* TODO: use Call instead of Spawn *)
+    ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
   ]
 
 (** Pthread functions. *)

From f2b002d664cab336f91b4032658de237168092ce Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 11 Sep 2023 14:31:01 +0300
Subject: [PATCH 53/56] Add CHANGELOG for v2.2.0

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a9531a5766..a126514852 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,27 @@
+## v2.2.0
+* TODO OCaml 5 (#1003, #1137).
+* TODO Library #1138
+* TODO refactor race #1136
+
+* Add `setjmp`/`longjmp` analysis (#887, #970, #1015, #1019).
+* Refactor race analysis to lazy distribution (#1084, #1089, #1016).
+* Add thread-unsafe library function call analysis (#723, #1082).
+* Add mutex type analysis and mutex API analysis (#800, #839, #1073).
+* Add interval set domain and string literals domain (#901, #966, #994, #1048).
+* Add affine equalities analysis (#592).
+* Add use-after-free analysis (#1050, #1114).
+* Add dead code elimination transformation (#850, #979).
+* Add taint analysis for partial contexts (#553, #952).
+* Add YAML witness validation via unassume (#796, #977, #1044, #1045, #1124).
+* Add incremental analysis rename detection (#774, #777).
+* Fix address sets unsoundness (#822, #967, #564, #1032, #998, #1031).
+* Fix thread escape analysis unsoundness (#939, #984, #1074, #1078).
+* Fix many incremental analysis issues (#627, #836, #835, #841, #932, #678, #942, #949, #950, #957, #955, #954, #960, #959, #1004, #558, #1010, #1091).
+* Fix server mode for abstract debugging (#983, #990, #997, #1000, #1001, #1013, #1018, #1017, #1026, #1027).
+* Add documentation for configuration JSON schema and OCaml API (#999, #1054, #1055, #1053).
+* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135).
+* Add OCaml 5.0 support (#945).
+
 ## v2.1.0
 Functionally equivalent to Goblint in SV-COMP 2023.
 

From 1128aba94f87b95031bef9929dea7294c78b880f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 11 Sep 2023 15:30:40 +0300
Subject: [PATCH 54/56] Fix deprecated File.exists? in update_suite.rb

---
 scripts/update_suite.rb | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index aeac526987..ca408a513a 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -41,7 +41,7 @@ def clearline
 
 $goblint = File.join(Dir.getwd,"goblint")
 goblintbyte = File.join(Dir.getwd,"goblint.byte")
-if File.exists?(goblintbyte) then
+if File.exist?(goblintbyte) then
   puts "Running the byte-code version! Continue? (y/n)"
   exit unless $stdin.gets()[0] == 'y'
   $goblint = goblintbyte
@@ -50,11 +50,11 @@ def clearline
 end
 $vrsn = `#{$goblint} --version`
 
-if not File.exists? "linux-headers" then
+if not File.exist? "linux-headers" then
   puts "Missing linux-headers, will download now!"
   `make headers`
 end
-has_linux_headers = File.exists? "linux-headers" # skip kernel tests if make headers failed (e.g. on opam-repository opam-ci where network is forbidden)
+has_linux_headers = File.exist? "linux-headers" # skip kernel tests if make headers failed (e.g. on opam-repository opam-ci where network is forbidden)
 
 #Command line parameters
 #Either only run a single test, or

From fd092e36fe2927adc284af3f37d900aa3ab1f763 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Edwin=20T=C3=B6r=C3=B6k?= <edwin.torok@cloud.com>
Date: Mon, 11 Sep 2023 15:23:23 +0100
Subject: [PATCH 55/56] goblint: fix lower bound on yaml
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

See build failure at https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/b49e6de20d0a04ef393c2e153d87d6e00f63c455

'opam-ci' would otherwise try 'yaml.1.0.0' which doesn't work:

```
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build goblint 2.1.0
+-
```

Signed-off-by: Edwin Török <edwin@etorok.net>
---
 dune-project | 2 +-
 goblint.opam | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/dune-project b/dune-project
index 1da7492d7d..54ed811ddf 100644
--- a/dune-project
+++ b/dune-project
@@ -42,7 +42,7 @@
     (sha (>= 1.12))
     cpu
     arg-complete
-    yaml
+    (yaml (>= 3.0.0))
     uuidm
     catapult
     catapult-file
diff --git a/goblint.opam b/goblint.opam
index ce7df4a3b0..04e4b27f9d 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -39,7 +39,7 @@ depends: [
   "sha" {>= "1.12"}
   "cpu"
   "arg-complete"
-  "yaml"
+  "yaml" {>= "3.0.0"}
   "uuidm"
   "catapult"
   "catapult-file"

From 70cd4e879945ad637827953e593010e93a954e50 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 12 Sep 2023 10:36:22 +0300
Subject: [PATCH 56/56] Fix Calloc indentation in base

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index b74555b7ad..6ab4015460 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2298,15 +2298,17 @@ struct
           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))
+              (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)))))]
+            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