From dac7983d06e05f4180c7d53513d5b03cfe2d01b3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 6 Sep 2023 10:05:31 +0200
Subject: [PATCH 001/104] Fix numbering

---
 .../{74-use_after_free => 78-use_after_free}/01-simple-uaf.c      | 0
 .../{74-use_after_free => 78-use_after_free}/02-conditional-uaf.c | 0
 .../{74-use_after_free => 78-use_after_free}/03-nested-ptr-uaf.c  | 0
 .../04-function-call-uaf.c                                        | 0
 .../05-uaf-free-in-wrapper-fun.c                                  | 0
 .../{74-use_after_free => 78-use_after_free}/06-uaf-struct.c      | 0
 .../{74-use_after_free => 78-use_after_free}/07-itc-double-free.c | 0
 .../08-itc-no-double-free.c                                       | 0
 .../{74-use_after_free => 78-use_after_free}/09-juliet-uaf.c      | 0
 .../10-juliet-double-free.c                                       | 0
 .../11-wrapper-funs-uaf.c                                         | 0
 .../12-multi-threaded-uaf.c                                       | 0
 .../13-multi-threaded-uaf-with-joined-thread.c                    | 0
 13 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/01-simple-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/02-conditional-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/03-nested-ptr-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/04-function-call-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/05-uaf-free-in-wrapper-fun.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/06-uaf-struct.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/07-itc-double-free.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/08-itc-no-double-free.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/09-juliet-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/10-juliet-double-free.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/11-wrapper-funs-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/12-multi-threaded-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 78-use_after_free}/13-multi-threaded-uaf-with-joined-thread.c (100%)

diff --git a/tests/regression/74-use_after_free/01-simple-uaf.c b/tests/regression/78-use_after_free/01-simple-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/01-simple-uaf.c
rename to tests/regression/78-use_after_free/01-simple-uaf.c
diff --git a/tests/regression/74-use_after_free/02-conditional-uaf.c b/tests/regression/78-use_after_free/02-conditional-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/02-conditional-uaf.c
rename to tests/regression/78-use_after_free/02-conditional-uaf.c
diff --git a/tests/regression/74-use_after_free/03-nested-ptr-uaf.c b/tests/regression/78-use_after_free/03-nested-ptr-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/03-nested-ptr-uaf.c
rename to tests/regression/78-use_after_free/03-nested-ptr-uaf.c
diff --git a/tests/regression/74-use_after_free/04-function-call-uaf.c b/tests/regression/78-use_after_free/04-function-call-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/04-function-call-uaf.c
rename to tests/regression/78-use_after_free/04-function-call-uaf.c
diff --git a/tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c b/tests/regression/78-use_after_free/05-uaf-free-in-wrapper-fun.c
similarity index 100%
rename from tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c
rename to tests/regression/78-use_after_free/05-uaf-free-in-wrapper-fun.c
diff --git a/tests/regression/74-use_after_free/06-uaf-struct.c b/tests/regression/78-use_after_free/06-uaf-struct.c
similarity index 100%
rename from tests/regression/74-use_after_free/06-uaf-struct.c
rename to tests/regression/78-use_after_free/06-uaf-struct.c
diff --git a/tests/regression/74-use_after_free/07-itc-double-free.c b/tests/regression/78-use_after_free/07-itc-double-free.c
similarity index 100%
rename from tests/regression/74-use_after_free/07-itc-double-free.c
rename to tests/regression/78-use_after_free/07-itc-double-free.c
diff --git a/tests/regression/74-use_after_free/08-itc-no-double-free.c b/tests/regression/78-use_after_free/08-itc-no-double-free.c
similarity index 100%
rename from tests/regression/74-use_after_free/08-itc-no-double-free.c
rename to tests/regression/78-use_after_free/08-itc-no-double-free.c
diff --git a/tests/regression/74-use_after_free/09-juliet-uaf.c b/tests/regression/78-use_after_free/09-juliet-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/09-juliet-uaf.c
rename to tests/regression/78-use_after_free/09-juliet-uaf.c
diff --git a/tests/regression/74-use_after_free/10-juliet-double-free.c b/tests/regression/78-use_after_free/10-juliet-double-free.c
similarity index 100%
rename from tests/regression/74-use_after_free/10-juliet-double-free.c
rename to tests/regression/78-use_after_free/10-juliet-double-free.c
diff --git a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/78-use_after_free/11-wrapper-funs-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/11-wrapper-funs-uaf.c
rename to tests/regression/78-use_after_free/11-wrapper-funs-uaf.c
diff --git a/tests/regression/74-use_after_free/12-multi-threaded-uaf.c b/tests/regression/78-use_after_free/12-multi-threaded-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/12-multi-threaded-uaf.c
rename to tests/regression/78-use_after_free/12-multi-threaded-uaf.c
diff --git a/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c b/tests/regression/78-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
similarity index 100%
rename from tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
rename to tests/regression/78-use_after_free/13-multi-threaded-uaf-with-joined-thread.c

From b3d9fe1ad02a2fd84455af118a3797922ba976d5 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 6 Sep 2023 11:07:26 +0200
Subject: [PATCH 002/104] Set the global SV-COMP analysis state vars at all
 necessary places

---
 src/analyses/base.ml           | 28 ++++++++++++++++++++--------
 src/analyses/memLeak.ml        | 12 +++++++++---
 src/analyses/memOutOfBounds.ml |  5 ++++-
 3 files changed, 33 insertions(+), 12 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index f237ca8296..79ac13b861 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1050,10 +1050,16 @@ struct
     | Mem n, ofs -> begin
         match (eval_rv a gs st n) with
         | Address adr ->
-          (if AD.is_null adr
-           then M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"
-           else if AD.may_be_null adr
-           then M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer");
+          (
+            if AD.is_null adr then (
+              AnalysisState.svcomp_may_invalid_deref := true;
+              M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"
+            )
+            else if AD.may_be_null adr then (
+              AnalysisState.svcomp_may_invalid_deref := true;
+              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
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
@@ -2023,12 +2029,18 @@ struct
     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. 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
+      if Q.LS.is_top points_to_set then (
+        AnalysisState.svcomp_may_invalid_free := true;
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590; CWE 761] "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 (
+        AnalysisState.svcomp_may_invalid_free := true;
         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) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then
+      )
+      else if Q.LS.exists (fun (_, o) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then (
+        AnalysisState.svcomp_may_invalid_free := true;
         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) =
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 99df5695a7..688ce1024a 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -19,15 +19,21 @@ struct
 
   (* HELPER FUNCTIONS *)
   let warn_for_multi_threaded ctx =
-    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
+    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then (
+      AnalysisState.svcomp_may_invalid_memtrack := true;
       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
       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
+      | true, Some exp ->
+        AnalysisState.svcomp_may_invalid_memtrack := true;
+        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
+      | _ ->
+        AnalysisState.svcomp_may_invalid_memtrack := true;
+        M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
 
   (* TRANSFER FUNCTIONS *)
   let return ctx (exp:exp option) (f:fundec) : D.t =
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 0e93adb295..a7e95282fd 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -194,7 +194,10 @@ struct
           IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
       end
     | _ ->
-      M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
+      (
+        AnalysisState.svcomp_may_invalid_deref :=true;
+        M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr
+      );
       IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
 
   and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval =

From 46ae6ee1d5bfacbed5ced3b475249d724d540601 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 6 Sep 2023 16:43:53 +0200
Subject: [PATCH 003/104] Add extra parentheses in witness.ml for memory safety
 result generation

---
 src/witness/witness.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 264e0bc066..31034a2d9a 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -512,7 +512,7 @@ struct
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_free then
+      if not !AnalysisState.svcomp_may_invalid_free then (
         let module TaskResult =
         struct
           module Arg = Arg
@@ -523,7 +523,7 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      else (
+      ) else (
         let module TaskResult =
         struct
           module Arg = TrivialArg
@@ -542,7 +542,7 @@ struct
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_deref then
+      if not !AnalysisState.svcomp_may_invalid_deref then (
         let module TaskResult =
         struct
           module Arg = Arg
@@ -553,7 +553,7 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      else (
+      ) else (
         let module TaskResult =
         struct
           module Arg = TrivialArg
@@ -572,7 +572,7 @@ struct
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_memtrack then
+      if not !AnalysisState.svcomp_may_invalid_memtrack then (
         let module TaskResult =
         struct
           module Arg = Arg
@@ -583,7 +583,7 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      else (
+      ) else (
         let module TaskResult =
         struct
           module Arg = TrivialArg

From d4ef55594e2f388febfb31e598e47691b7dafc90 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 6 Sep 2023 17:21:58 +0200
Subject: [PATCH 004/104] Add quick and dirty workaround attempt for working
 with SV-COMP's memory-safety category

---
 src/autoTune.ml           |  1 +
 src/witness/svcomp.ml     |  1 +
 src/witness/svcompSpec.ml | 14 ++++++++----
 src/witness/witness.ml    | 46 ++++++++++++++++++++++++++++++++-------
 4 files changed, 50 insertions(+), 12 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index d532081799..9e3508ccd2 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -226,6 +226,7 @@ let focusOnSpecification () =
   (* TODO: Finish these two below later *)
   | ValidDeref
   | ValidMemtrack -> ()
+  | MemorySafety -> () (* TODO: This is here for now just to complete the pattern match *)
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index f1ee18ed72..15d41c0210 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -55,6 +55,7 @@ struct
         | ValidFree -> "valid-free"
         | ValidDeref -> "valid-deref"
         | ValidMemtrack -> "valid-memtrack"
+        | MemorySafety -> "memory-safety" (* TODO: Currently here only to complete the pattern match *)
       in
       "false(" ^ result_spec ^ ")"
     | Unknown -> "unknown"
diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index 8dafb8873c..f066610953 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -9,10 +9,11 @@ type t =
   | ValidFree
   | ValidDeref
   | ValidMemtrack
+  | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
 
 let of_string s =
   let s = String.strip s in
-  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
   if Str.string_match regexp_negated s 0 then
     let global_not = Str.matched_group 1 s in
@@ -28,13 +29,17 @@ let of_string s =
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
   else if Str.string_match regexp s 0 then
-    let global = Str.matched_group 1 s in
-    if global = "valid-free" then
+    let global1 = Str.matched_group 1 s in
+    let global2 = Str.matched_group 2 s in
+    let global3 = Str.matched_group 3 s in
+    if global1 = "valid-free" && global2 = "valid-deref" && global3 = "valid-memtrack" then
+      MemorySafety
+      (* if global = "valid-free" then
       ValidFree
     else if global = "valid-deref" then
       ValidDeref
     else if global = "valid-memtrack" then
-      ValidMemtrack
+          ValidMemtrack *)
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
   else
@@ -65,5 +70,6 @@ let to_string spec =
     | ValidFree -> "valid-free", false
     | ValidDeref -> "valid-deref", false
     | ValidMemtrack -> "valid-memtrack", false
+    | MemorySafety -> "memory-safety", false (* TODO: That's false, it's currently here just to complete the pattern match *)
   in
   print_output spec_str is_neg
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 31034a2d9a..437ba187ae 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -505,8 +505,8 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree ->
-      let module TrivialArg =
+    | ValidFree (*->*)
+    (* let module TrivialArg =
       struct
         include Arg
         let next _ = []
@@ -534,9 +534,9 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      )
-    | ValidDeref ->
-      let module TrivialArg =
+        ) *)
+    | ValidDeref (*->*)
+    (* let module TrivialArg =
       struct
         include Arg
         let next _ = []
@@ -564,9 +564,9 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      )
-    | ValidMemtrack ->
-      let module TrivialArg =
+        ) *)
+    | ValidMemtrack (*->*)
+    (* let module TrivialArg =
       struct
         include Arg
         let next _ = []
@@ -583,6 +583,36 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
+        ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+        ) *)
+    | MemorySafety ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_free || not !AnalysisState.svcomp_may_invalid_deref || not !AnalysisState.svcomp_may_invalid_memtrack then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
       ) else (
         let module TaskResult =
         struct

From 2fb4d743374fd4322ad2fa2ce98bcaf91d8870ee Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 6 Sep 2023 18:59:51 +0200
Subject: [PATCH 005/104] Use logical AND and not OR for the memory-safety
 category in witness

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

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 437ba187ae..66a62d1b03 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -602,7 +602,7 @@ struct
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_free || not !AnalysisState.svcomp_may_invalid_deref || not !AnalysisState.svcomp_may_invalid_memtrack then (
+      if not !AnalysisState.svcomp_may_invalid_free && not !AnalysisState.svcomp_may_invalid_deref && not !AnalysisState.svcomp_may_invalid_memtrack then (
         let module TaskResult =
         struct
           module Arg = Arg

From 9cbf2ab8d10c064a1c1714e700b3b405478b81ae Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sat, 9 Sep 2023 23:13:03 +0200
Subject: [PATCH 006/104] Add util function for setting mem safety global vars

Make sure to do this only if we're in postsolving
---
 src/analyses/base.ml           | 10 +++++-----
 src/analyses/memLeak.ml        |  7 ++++---
 src/analyses/memOutOfBounds.ml | 13 +++++++------
 src/analyses/useAfterFree.ml   | 17 ++++++-----------
 src/util/analysisStateUtil.ml  | 11 +++++++++++
 5 files changed, 33 insertions(+), 25 deletions(-)
 create mode 100644 src/util/analysisStateUtil.ml

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 79ac13b861..0cdcf98fc0 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1052,11 +1052,11 @@ struct
         | Address adr ->
           (
             if AD.is_null adr then (
-              AnalysisState.svcomp_may_invalid_deref := true;
+              AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
               M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"
             )
             else if AD.may_be_null adr then (
-              AnalysisState.svcomp_may_invalid_deref := true;
+              AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
               M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer"
             )
           );
@@ -2030,15 +2030,15 @@ struct
     | Address a ->
       let points_to_set = addrToLvalSet a in
       if Q.LS.is_top points_to_set then (
-        AnalysisState.svcomp_may_invalid_free := true;
+        AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590; CWE 761] "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 (
-        AnalysisState.svcomp_may_invalid_free := true;
+        AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         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) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then (
-        AnalysisState.svcomp_may_invalid_free := true;
+        AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         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
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 688ce1024a..0ea4fc96b1 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -3,6 +3,7 @@
 open GoblintCil
 open Analyses
 open MessageCategory
+open AnalysisStateUtil
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
 
@@ -20,7 +21,7 @@ struct
   (* HELPER FUNCTIONS *)
   let warn_for_multi_threaded ctx =
     if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then (
-      AnalysisState.svcomp_may_invalid_memtrack := true;
+      set_mem_safety_flag InvalidMemTrack;
       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"
     )
 
@@ -29,10 +30,10 @@ struct
     if not @@ D.is_empty state then
       match assert_exp_imprecise, exp with
       | true, Some exp ->
-        AnalysisState.svcomp_may_invalid_memtrack := true;
+        AnalysisStateUtil.set_mem_safety_flag InvalidMemTrack;
         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
       | _ ->
-        AnalysisState.svcomp_may_invalid_memtrack := true;
+        AnalysisStateUtil.set_mem_safety_flag InvalidMemTrack;
         M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
 
   (* TRANSFER FUNCTIONS *)
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index a7e95282fd..a5cf7d2ca2 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -1,6 +1,7 @@
 open GoblintCil
 open Analyses
 open MessageCategory
+open AnalysisStateUtil
 
 module AS = AnalysisState
 module VDQ = ValueDomainQueries
@@ -195,7 +196,7 @@ struct
       end
     | _ ->
       (
-        AnalysisState.svcomp_may_invalid_deref :=true;
+        set_mem_safety_flag InvalidDeref;
         M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr
       );
       IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
@@ -229,12 +230,12 @@ struct
     | Some t ->
       begin match VDQ.ID.is_top ptr_size with
         | true ->
-          AS.svcomp_may_invalid_deref := true;
+          set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a not known. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp
         | false ->
           let offs = `Lifted addr_offs in
           if ptr_size < offs then begin
-            AS.svcomp_may_invalid_deref := true;
+            set_mem_safety_flag InvalidDeref;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size VDQ.ID.pretty offs
           end
       end
@@ -287,14 +288,14 @@ struct
           in
           begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size_with_addr_size with
             | true, _ ->
-              AS.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp
             | _, true ->
-              AS.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp
             | false, false ->
               if ptr_size < offset_size_with_addr_size then begin
-                AS.svcomp_may_invalid_deref := true;
+                set_mem_safety_flag InvalidDeref;
                 M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp VDQ.ID.pretty ptr_size VDQ.ID.pretty offset_size_with_addr_size
               end
           end
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 9af1b8ca7a..9dac016ce5 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -3,6 +3,7 @@
 open GoblintCil
 open Analyses
 open MessageCategory
+open AnalysisStateUtil
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
 module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet)
@@ -24,12 +25,6 @@ struct
 
   (* HELPER FUNCTIONS *)
 
-  let set_global_svcomp_var is_double_free =
-    if is_double_free then
-      AnalysisState.svcomp_may_invalid_free := true
-    else
-      AnalysisState.svcomp_may_invalid_deref := true
-
   let get_current_threadid ctx =
     ctx.ask Queries.CurrentThreadId
 
@@ -65,23 +60,23 @@ struct
       | `Lifted current ->
         let possibly_started = G.exists (possibly_started current) freeing_threads in
         if possibly_started then begin
-          set_global_svcomp_var is_double_free;
+          if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. %s might occur" CilType.Varinfo.pretty heap_var bug_name
         end
         else begin
           let current_is_unique = ThreadId.Thread.is_unique current in
           let any_equal_current threads = G.exists (equal_current current) threads in
           if not current_is_unique && any_equal_current freeing_threads then begin
-            set_global_svcomp_var is_double_free;
+            if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
           end
           else if D.mem heap_var ctx.local then begin
-            set_global_svcomp_var is_double_free;
+            if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
           end
         end
       | `Top ->
-        set_global_svcomp_var is_double_free;
+        if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
         M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
       | `Bot ->
         M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
@@ -110,7 +105,7 @@ struct
         | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
           let warn_for_heap_var var =
             if D.mem var state then begin
-              set_global_svcomp_var is_double_free;
+              if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" var.vname transfer_fn_name
             end
           in
diff --git a/src/util/analysisStateUtil.ml b/src/util/analysisStateUtil.ml
new file mode 100644
index 0000000000..25914f8c8e
--- /dev/null
+++ b/src/util/analysisStateUtil.ml
@@ -0,0 +1,11 @@
+type mem_safety_violation =
+  | InvalidFree
+  | InvalidDeref
+  | InvalidMemTrack
+
+let set_mem_safety_flag violation_type =
+  if !AnalysisState.postsolving then
+    match violation_type with
+    | InvalidFree -> AnalysisState.svcomp_may_invalid_free := true
+    | InvalidDeref -> AnalysisState.svcomp_may_invalid_deref := true
+    | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true
\ No newline at end of file

From 3258cce90b88ea14db99c5e6466b43b7fd8a01a5 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sat, 9 Sep 2023 23:35:54 +0200
Subject: [PATCH 007/104] Don't warn for pointers that only contain strings in
 their pts

---
 src/analyses/memOutOfBounds.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index a5cf7d2ca2..4c2576ec24 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -161,6 +161,13 @@ struct
       let remaining_offset = offs_to_idx typ o in
       IntDomain.IntDomTuple.add bytes_offset remaining_offset
 
+  let ptr_only_has_str_addr ctx ptr =
+    ctx.ask (Queries.MayPointTo ptr)
+    |> VDQ.LS.elements
+    |> List.map (fun (v, o) -> ValueDomain.Addr.of_mval (v, ValueDomain.Addr.Offs.of_exp o))
+    |> ValueDomain.AD.of_list
+    |> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false)
+
   let rec get_addr_offs ctx ptr =
     match ctx.ask (Queries.MayPointTo ptr) with
     | a when not (VDQ.LS.is_top a) ->
@@ -202,7 +209,8 @@ struct
       IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
 
   and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval =
-    if not @@ lval_contains_a_ptr lval then ()
+    (* If the lval does not contain a pointer or if it does contain a pointer, but only points to string addresses, then no need to WARN *)
+    if (not @@ lval_contains_a_ptr lval) || ptr_only_has_str_addr ctx (Lval lval) then ()
     else
       (* If the lval doesn't indicate an explicit dereference, we still need to check for an implicit dereference *)
       (* An implicit dereference is, e.g., printf("%p", ptr), where ptr is a pointer *)

From 0881fb786b7a4a17c0fd5adadc50378580c99a73 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sat, 9 Sep 2023 23:39:05 +0200
Subject: [PATCH 008/104] Set global mem safety flags upon array oob as well

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

diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
index c099a94f96..2f91e47663 100644
--- a/src/cdomains/arrayDomain.ml
+++ b/src/cdomains/arrayDomain.ml
@@ -787,14 +787,19 @@ let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l)
     | Some true, Some true -> (* Certainly in bounds on both sides.*)
       ()
     | Some true, Some false -> (* The following matching differentiates the must and may cases*)
+      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
       M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "Must access array past end"
     | Some true, None ->
+      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
       M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "May access array past end"
     | Some false, Some true ->
+      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
       M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "Must access array before start"
     | None, Some true ->
+      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
       M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "May access array before start"
     | _ ->
+      AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
       M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.unknown "May access array out of bounds"
   else ()
 

From b9faa8f039a6ad5faeb2ea16483c9c1b179b71da Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sat, 9 Sep 2023 23:47:58 +0200
Subject: [PATCH 009/104] Cast pointer arithmetic offsets without using
 Option.get

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

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 4c2576ec24..a2c180a453 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -138,11 +138,12 @@ struct
 
   let eval_ptr_offset_in_binop ctx exp ptr_contents_typ =
     let eval_offset = ctx.ask (Queries.EvalInt exp) in
-    let eval_offset = Option.get @@ VDQ.ID.to_int eval_offset in
-    let eval_offset = VDQ.ID.of_int (Cilfacade.ptrdiff_ikind ()) eval_offset in
     let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in
     match eval_offset with
-    | `Lifted i -> `Lifted (IntDomain.IntDomTuple.mul i ptr_contents_typ_size_in_bytes)
+    | `Lifted i ->
+      (* The offset must be casted to ptrdiff_ikind in order to have matching ikinds for the multiplication below *)
+      let casted_offset = IntDomain.IntDomTuple.cast_to (Cilfacade.ptrdiff_ikind ()) i in
+      `Lifted (IntDomain.IntDomTuple.mul casted_offset ptr_contents_typ_size_in_bytes)
     | `Top -> `Top
     | `Bot -> `Bot
 

From 8a6cf0a10258cd6c433f6067111b10f93323002d Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sun, 10 Sep 2023 02:11:41 +0200
Subject: [PATCH 010/104] Check and warn everywhere for a top points-to set in
 memOutOfBounds

---
 src/analyses/memOutOfBounds.ml | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index a2c180a453..781c48d8e9 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -88,7 +88,9 @@ struct
     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.for_all (fun (v, _) -> ctx.ask (Queries.IsHeapVar v)) a
-    | _ -> false
+    | _ ->
+      M.warn "Pointer %a has a points-to set of top. An invalid memory access might occur" d_exp ptr;
+      false
 
   let get_size_of_ptr_target ctx ptr =
     if points_to_heap_only ctx ptr then
@@ -124,7 +126,7 @@ struct
             ) x xs
         end
       | _ ->
-        M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
+        M.warn "Pointer %a has a points-to set of top. An invalid memory access might occur" d_exp ptr;
         VDQ.ID.top ()
 
   let get_ptr_deref_type ptr_typ =
@@ -163,11 +165,16 @@ struct
       IntDomain.IntDomTuple.add bytes_offset remaining_offset
 
   let ptr_only_has_str_addr ctx ptr =
-    ctx.ask (Queries.MayPointTo ptr)
-    |> VDQ.LS.elements
-    |> List.map (fun (v, o) -> ValueDomain.Addr.of_mval (v, ValueDomain.Addr.Offs.of_exp o))
-    |> ValueDomain.AD.of_list
-    |> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false)
+    match ctx.ask (Queries.MayPointTo ptr) with
+    | a when not (VDQ.LS.is_top a) ->
+      VDQ.LS.elements a
+      |> List.map (fun (v, o) -> ValueDomain.Addr.of_mval (v, ValueDomain.Addr.Offs.of_exp o))
+      |> ValueDomain.AD.of_list
+      |> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false)
+    | _ ->
+      M.warn "Pointer %a has a points-to set of top. An invalid memory access might occur" d_exp ptr;
+      (* Intuition: if the points-to set is top, then we don't know with certainty if there are only string addresses inside *)
+      false
 
   let rec get_addr_offs ctx ptr =
     match ctx.ask (Queries.MayPointTo ptr) with
@@ -203,10 +210,8 @@ struct
           IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
       end
     | _ ->
-      (
-        set_mem_safety_flag InvalidDeref;
-        M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr
-      );
+      set_mem_safety_flag InvalidDeref;
+      M.warn "Pointer %a has a points-to set of top. An invalid memory access might occur" d_exp ptr;
       IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
 
   and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval =

From 29f13a281aa183722b375c163d427c434d70dcbd Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sun, 10 Sep 2023 14:06:34 +0200
Subject: [PATCH 011/104] Simplify string address check and remove extra
 warning

---
 src/analyses/memOutOfBounds.ml | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 781c48d8e9..de18021278 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -88,9 +88,7 @@ struct
     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.for_all (fun (v, _) -> ctx.ask (Queries.IsHeapVar v)) a
-    | _ ->
-      M.warn "Pointer %a has a points-to set of top. An invalid memory access might occur" d_exp ptr;
-      false
+    | _ -> false
 
   let get_size_of_ptr_target ctx ptr =
     if points_to_heap_only ctx ptr then
@@ -165,16 +163,14 @@ struct
       IntDomain.IntDomTuple.add bytes_offset remaining_offset
 
   let ptr_only_has_str_addr ctx ptr =
-    match ctx.ask (Queries.MayPointTo ptr) with
-    | a when not (VDQ.LS.is_top a) ->
-      VDQ.LS.elements a
-      |> List.map (fun (v, o) -> ValueDomain.Addr.of_mval (v, ValueDomain.Addr.Offs.of_exp o))
-      |> ValueDomain.AD.of_list
-      |> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false)
-    | _ ->
-      M.warn "Pointer %a has a points-to set of top. An invalid memory access might occur" d_exp ptr;
-      (* Intuition: if the points-to set is top, then we don't know with certainty if there are only string addresses inside *)
-      false
+    match ctx.ask (Queries.EvalValue ptr) with
+    | a when not (Queries.VD.is_top a) ->
+      begin match a with
+        | Address a -> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false) a
+        | _ -> false
+      end
+    (* Intuition: if ptr evaluates to top, it could all sorts of things and not only string addresses *)
+    | _ -> false
 
   let rec get_addr_offs ctx ptr =
     match ctx.ask (Queries.MayPointTo ptr) with

From 7bdce29722c52c4366f0ff7457ad2b6c12f2ebeb Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Sun, 10 Sep 2023 14:17:25 +0200
Subject: [PATCH 012/104] Add check for dereferencing a pointer containing an
 unknown address

---
 src/analyses/memOutOfBounds.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index de18021278..9f9708335f 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -162,6 +162,22 @@ struct
       let remaining_offset = offs_to_idx typ o in
       IntDomain.IntDomTuple.add bytes_offset remaining_offset
 
+  let check_unknown_addr_deref ctx ptr =
+    let may_contain_unknown_addr =
+      match ctx.ask (Queries.EvalValue ptr) with
+      | a when not (Queries.VD.is_top a) ->
+        begin match a with
+          | Address a -> ValueDomain.AD.may_be_unknown a
+          | _ -> false
+        end
+      (* Intuition: if ptr evaluates to top, it could potentially evaluate to the unknown address *)
+      | _ -> true
+    in
+    if may_contain_unknown_addr then begin
+      set_mem_safety_flag InvalidDeref;
+      M.warn ~category:(Behavior (Undefined Other)) "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr
+    end
+
   let ptr_only_has_str_addr ctx ptr =
     match ctx.ask (Queries.EvalValue ptr) with
     | a when not (Queries.VD.is_top a) ->
@@ -230,6 +246,7 @@ struct
         end
 
   and check_no_binop_deref ctx lval_exp =
+    check_unknown_addr_deref ctx lval_exp;
     let behavior = Undefined MemoryOutOfBoundsAccess in
     let cwe_number = 823 in
     let ptr_size = get_size_of_ptr_target ctx lval_exp in
@@ -276,6 +293,7 @@ struct
     | AddrOf lval -> check_lval_for_oob_access ctx ~is_implicitly_derefed lval
 
   and check_binop_exp ctx binop e1 e2 t =
+    check_unknown_addr_deref ctx e1;
     let binopexp = BinOp (binop, e1, e2, t) in
     let behavior = Undefined MemoryOutOfBoundsAccess in
     let cwe_number = 823 in

From 3c014186d9f77bec2e734828aee0c1caf8a24b6b Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 13 Sep 2023 15:14:54 +0200
Subject: [PATCH 013/104] Remove unused function

---
 src/analyses/memOutOfBounds.ml | 27 ---------------------------
 1 file changed, 27 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 9f9708335f..01bc12d7cb 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -23,33 +23,6 @@ struct
   let intdom_of_int x =
     IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
 
-  let to_index ?typ offs =
-    let idx_of_int x =
-      IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (x / 8))
-    in
-    let rec offset_to_index_offset ?typ offs = match offs with
-      | `NoOffset -> idx_of_int 0
-      | `Field (field, o) ->
-        let field_as_offset = Field (field, NoOffset) in
-        let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset  in
-        let bits_offset = idx_of_int bits_offset in
-        let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
-        IntDomain.IntDomTuple.add bits_offset remaining_offset
-      | `Index (x, o) ->
-        let (item_typ, item_size_in_bits) =
-          match Option.map unrollType typ with
-          | Some TArray(item_typ, _, _) ->
-            let item_size_in_bits = bitsSizeOf item_typ in
-            (Some item_typ, idx_of_int item_size_in_bits)
-          | _ ->
-            (None, IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ())
-        in
-        let bits_offset = IntDomain.IntDomTuple.mul item_size_in_bits x in
-        let remaining_offset = offset_to_index_offset ?typ:item_typ o in
-        IntDomain.IntDomTuple.add bits_offset remaining_offset
-    in
-    offset_to_index_offset ?typ offs
-
   let rec exp_contains_a_ptr (exp:exp) =
     match exp with
     | Const _

From 15f782b9efd276da84cbbf8121f04eb2e47101b8 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 13 Sep 2023 15:25:44 +0200
Subject: [PATCH 014/104] Add exception handling for intdom arithmetic in
 memOutOfBounds

---
 src/analyses/memOutOfBounds.ml | 33 +++++++++++++++++++++++++--------
 1 file changed, 25 insertions(+), 8 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 01bc12d7cb..61e1b1a808 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -77,7 +77,11 @@ struct
               let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in
               let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in
               begin match ctx.ask (Queries.EvalLength ptr) with
-                | `Lifted arr_len -> `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len)
+                | `Lifted arr_len ->
+                  begin
+                    try `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len)
+                    with IntDomain.ArithmeticOnIntegerBot _ -> VDQ.ID.bot ()
+                  end
                 | `Bot -> VDQ.ID.bot ()
                 | `Top -> VDQ.ID.top ()
               end
@@ -116,7 +120,10 @@ struct
     | `Lifted i ->
       (* The offset must be casted to ptrdiff_ikind in order to have matching ikinds for the multiplication below *)
       let casted_offset = IntDomain.IntDomTuple.cast_to (Cilfacade.ptrdiff_ikind ()) i in
-      `Lifted (IntDomain.IntDomTuple.mul casted_offset ptr_contents_typ_size_in_bytes)
+      begin
+        try `Lifted (IntDomain.IntDomTuple.mul casted_offset ptr_contents_typ_size_in_bytes)
+        with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
+      end
     | `Top -> `Top
     | `Bot -> `Bot
 
@@ -128,12 +135,18 @@ struct
       let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in
       let bytes_offset = intdom_of_int (bits_offset / 8) in
       let remaining_offset = offs_to_idx field.ftype o in
-      IntDomain.IntDomTuple.add bytes_offset remaining_offset
+      begin
+        try IntDomain.IntDomTuple.add bytes_offset remaining_offset
+        with IntDomain.ArithmeticOnIntegerBot _ -> IntDomain.IntDomTuple.bot_of @@ Cilfacade.ptrdiff_ikind ()
+      end
     | `Index (x, o) ->
-      let typ_size_in_bytes = size_of_type_in_bytes typ in
-      let bytes_offset = IntDomain.IntDomTuple.mul typ_size_in_bytes x in
-      let remaining_offset = offs_to_idx typ o in
-      IntDomain.IntDomTuple.add bytes_offset remaining_offset
+      begin try
+          let typ_size_in_bytes = size_of_type_in_bytes typ in
+          let bytes_offset = IntDomain.IntDomTuple.mul typ_size_in_bytes x in
+          let remaining_offset = offs_to_idx typ o in
+          IntDomain.IntDomTuple.add bytes_offset remaining_offset
+        with IntDomain.ArithmeticOnIntegerBot _ -> IntDomain.IntDomTuple.bot_of @@ Cilfacade.ptrdiff_ikind ()
+      end
 
   let check_unknown_addr_deref ctx ptr =
     let may_contain_unknown_addr =
@@ -283,7 +296,11 @@ struct
           let offset_size = eval_ptr_offset_in_binop ctx e2 t in
           (* Make sure to add the address offset to the binop offset *)
           let offset_size_with_addr_size = match offset_size with
-            | `Lifted os -> `Lifted (IntDomain.IntDomTuple.add os addr_offs)
+            | `Lifted os ->
+              begin
+                try `Lifted (IntDomain.IntDomTuple.add os addr_offs)
+                with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
+              end
             | `Top -> `Top
             | `Bot -> `Bot
           in

From 20433e34c968f8c413bb1042f1165f547a70f203 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 13 Sep 2023 17:15:58 +0200
Subject: [PATCH 015/104] Ignore info messages for test case 77/05 due to MacOS
 CI

---
 tests/regression/77-mem-oob/05-oob-implicit-deref.c | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/regression/77-mem-oob/05-oob-implicit-deref.c b/tests/regression/77-mem-oob/05-oob-implicit-deref.c
index 088493d3b9..8bec6a72e0 100644
--- a/tests/regression/77-mem-oob/05-oob-implicit-deref.c
+++ b/tests/regression/77-mem-oob/05-oob-implicit-deref.c
@@ -1,4 +1,8 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
+/*
+    Note: the "--disable warn.info" above is a temporary workaround,
+    since the GitHub CI seems to be considering Info messages as violations of NOWARN (cf. https://github.com/goblint/analyzer/issues/1151)
+*/
 #include <stdlib.h>
 #include <stdio.h>
 #include <string.h>

From 1116ef622f21fb53e82780317c19088c9bad25de Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 24 Sep 2023 14:22:35 +0200
Subject: [PATCH 016/104] No shortcut `meet` and `narrow` w/ int refinement

---
 src/domains/lattice.ml                         |  9 +++++++--
 .../regression/38-int-refinements/06-narrow.c  | 18 ++++++++++++++++++
 2 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/38-int-refinements/06-narrow.c

diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml
index 4cdaa8fb9f..841d1d61b7 100644
--- a/src/domains/lattice.ml
+++ b/src/domains/lattice.ml
@@ -151,10 +151,15 @@ end
 module HConsed (Base:S) =
 struct
   include Printable.HConsed (Base)
+
+  (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues *)
+  (* see https://github.com/goblint/analyzer/issues/1005 *)
+  let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never"
+
   let lift_f2 f x y = f (unlift x) (unlift y)
-  let narrow x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
+  let narrow x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
   let widen x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y)
-  let meet x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
+  let meet x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
   let join x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.join x y)
   let leq x y = (x.BatHashcons.tag == y.BatHashcons.tag) || lift_f2 Base.leq x y
   let is_top = lift_f Base.is_top
diff --git a/tests/regression/38-int-refinements/06-narrow.c b/tests/regression/38-int-refinements/06-narrow.c
new file mode 100644
index 0000000000..513e9dde60
--- /dev/null
+++ b/tests/regression/38-int-refinements/06-narrow.c
@@ -0,0 +1,18 @@
+// PARAM: --set ana.int.refinement fixpoint --enable ana.int.interval
+// FIXPOINT
+#include<assert.h>
+
+int g = 0;
+
+void main()
+{
+   int i = 0;
+   while (1) {
+      i++;
+      for (int j=0; j < 10; j++) {
+         if (i > 100) g = 1;
+      }
+      if (i>9) i=0;
+   }
+   return;
+}

From 2f691be58f2367cdf2f8fb51e7fcf947b0571df3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 24 Sep 2023 14:23:42 +0200
Subject: [PATCH 017/104] Make comment a bit longer

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

diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml
index 841d1d61b7..3e1207b8b1 100644
--- a/src/domains/lattice.ml
+++ b/src/domains/lattice.ml
@@ -152,7 +152,7 @@ module HConsed (Base:S) =
 struct
   include Printable.HConsed (Base)
 
-  (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues *)
+  (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
   (* see https://github.com/goblint/analyzer/issues/1005 *)
   let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never"
 

From dee2a60ba7855321f2d67513ca97be8cdbe3320d Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 01:02:38 +0200
Subject: [PATCH 018/104] Set SV-COMP memory safety global flags at all
 necessary locations

---
 src/analyses/base.ml           | 10 +++++---
 src/analyses/memLeak.ml        |  4 ++--
 src/analyses/memOutOfBounds.ml | 42 +++++++++++++++++-----------------
 src/analyses/useAfterFree.ml   |  6 +++--
 4 files changed, 34 insertions(+), 28 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index d9cfba7b18..a624fd0b40 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2027,12 +2027,16 @@ struct
     in
     match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
     | Address a ->
-      if AD.is_top a then
+      if AD.is_top a then (
+        AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         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 has_non_heap_var a then
+      ) else if has_non_heap_var a then (
+        AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         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 has_non_zero_offset a then
+      ) else if has_non_zero_offset a then (
+        AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         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
 
 
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 56cbbbff3d..eb38b97a1c 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -30,10 +30,10 @@ struct
     if not @@ D.is_empty state then
       match assert_exp_imprecise, exp with
       | true, Some exp ->
-        AnalysisStateUtil.set_mem_safety_flag InvalidMemTrack;
+        set_mem_safety_flag InvalidMemTrack;
         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
       | _ ->
-        AnalysisStateUtil.set_mem_safety_flag InvalidMemTrack;
+        set_mem_safety_flag InvalidMemTrack;
         M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
 
   (* TRANSFER FUNCTIONS *)
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 9ee022fe08..db86a63414 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -118,6 +118,7 @@ struct
           | x::xs -> List.fold_left VDQ.ID.join x xs
         end
       | _ ->
+        set_mem_safety_flag InvalidDeref;
         M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
         `Top
 
@@ -172,7 +173,7 @@ struct
       | _ -> true
     in
     if may_contain_unknown_addr then begin
-      (* set_mem_safety_flag InvalidDeref; *)
+      set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior (Undefined Other)) "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr
     end
 
@@ -201,15 +202,13 @@ struct
                   | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o
                   | _ -> false
                 ) a then (
-                (* TODO: Uncomment once staging-memsafety branch changes are applied *)
-                (* set_mem_safety_flag InvalidDeref; *)
+                set_mem_safety_flag InvalidDeref;
                 M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr
               ) else if VDQ.AD.exists (function
                   | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o
                   | _ -> false
                 ) a then (
-                (* TODO: Uncomment once staging-memsafety branch changes are applied *)
-                (* set_mem_safety_flag InvalidDeref; *)
+                set_mem_safety_flag InvalidDeref;
                 M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr
               );
               (* Offset should be the same for all elements in the points-to set *)
@@ -224,7 +223,7 @@ struct
           ID.top_of @@ Cilfacade.ptrdiff_ikind ()
       end
     | _ ->
-      (* set_mem_safety_flag InvalidDeref; *)
+      set_mem_safety_flag InvalidDeref;
       M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
       ID.top_of @@ Cilfacade.ptrdiff_ikind ()
 
@@ -259,10 +258,10 @@ struct
     | Some t ->
       begin match ptr_size, addr_offs with
         | `Top, _ ->
-          AS.svcomp_may_invalid_deref := true;
+          set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp
         | `Bot, _ ->
-          AS.svcomp_may_invalid_deref := true;
+          set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp
         | `Lifted ps, ao ->
           let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in
@@ -270,11 +269,11 @@ struct
           let ptr_size_lt_offs = ID.lt casted_ps casted_ao in
           begin match ID.to_bool ptr_size_lt_offs with
             | Some true ->
-              AnalysisState.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao
             | Some false -> ()
             | None ->
-              AnalysisState.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao
           end
       end
@@ -334,16 +333,16 @@ struct
           in
           begin match ptr_size, offset_size_with_addr_size with
             | `Top, _ ->
-              AS.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp
             | _, `Top ->
-              AS.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp
             | `Bot, _ ->
-              AS.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp
             | _, `Bot ->
-              AS.svcomp_may_invalid_deref := true;
+              set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp
             | `Lifted ps, `Lifted o ->
               let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in
@@ -351,11 +350,11 @@ struct
               let ptr_size_lt_offs = ID.lt casted_ps casted_o in
               begin match ID.to_bool ptr_size_lt_offs with
                 | Some true ->
-                  AS.svcomp_may_invalid_deref := true;
+                  set_mem_safety_flag InvalidDeref;
                   M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o
                 | Some false -> ()
                 | None ->
-                  AnalysisState.svcomp_may_invalid_deref := true;
+                  set_mem_safety_flag InvalidDeref;
                   M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o
               end
           end
@@ -372,15 +371,16 @@ struct
     let addr_offs = get_addr_offs ctx dest in
     match dest_size, eval_n with
     | `Top, _ ->
-      AnalysisState.svcomp_may_invalid_deref := true;
+      set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name
     | _, `Top ->
-      AnalysisState.svcomp_may_invalid_deref := true;
+      set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name
     | `Bot, _ ->
-      AnalysisState.svcomp_may_invalid_deref := true;
+      set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name
     | _, `Bot ->
+      set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name
     | `Lifted ds, `Lifted en ->
       let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
@@ -389,11 +389,11 @@ struct
       let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in
       begin match ID.to_bool dest_size_lt_count with
         | Some true ->
-          AnalysisState.svcomp_may_invalid_deref := true;
+          set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en
         | Some false -> ()
         | None ->
-          AnalysisState.svcomp_may_invalid_deref := true;
+          set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name
       end
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index dfbab87a29..2f4b54f000 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -76,7 +76,7 @@ struct
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
           end
           else if HeapVars.mem heap_var (snd ctx.local) then begin
-            set_global_svcomp_var is_double_free;
+            if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
           end
         end
@@ -110,8 +110,10 @@ struct
       begin match ctx.ask (Queries.MayPointTo lval_to_query) with
         | ad when not (Queries.AD.is_top ad) ->
           let warn_for_heap_var v =
-            if HeapVars.mem v (snd state) then
+            if HeapVars.mem v (snd state) then begin
+              if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name
+            end
           in
           let pointed_to_heap_vars =
             Queries.AD.fold (fun addr vars ->

From da45e40b56d3a049656cfb2993b462e6b797c5ac Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 01:05:18 +0200
Subject: [PATCH 019/104] Clean up UAF analysis a bit

---
 src/analyses/useAfterFree.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 2f4b54f000..a28591e273 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -15,7 +15,7 @@ module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted
 
 module Spec : Analyses.MCPSpec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "useAfterFree"
 
@@ -24,7 +24,6 @@ struct
   module G = ThreadIdToJoinedThreadsMap
   module V = VarinfoV
 
-  (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *)
   let context _ _ = ()
 
 
@@ -176,9 +175,6 @@ struct
     warn_exp_might_contain_freed "branch" ctx exp;
     ctx.local
 
-  let body ctx (f:fundec) : D.t =
-    ctx.local
-
   let return ctx (exp:exp option) (f:fundec) : D.t =
     Option.iter (fun x -> warn_exp_might_contain_freed "return" ctx x) exp;
     ctx.local
@@ -248,9 +244,6 @@ struct
       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 ()
 

From 1335123d60b556e9759a4e4147d72095142a9452 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 09:45:49 +0200
Subject: [PATCH 020/104] Recognize mem-safety props in any order

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

diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index f066610953..fbe206dabb 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -32,7 +32,8 @@ let of_string s =
     let global1 = Str.matched_group 1 s in
     let global2 = Str.matched_group 2 s in
     let global3 = Str.matched_group 3 s in
-    if global1 = "valid-free" && global2 = "valid-deref" && global3 = "valid-memtrack" then
+    let mem_safety_props = ["valid-free"; "valid-deref"; "valid-memtrack";] in
+    if (global1 <> global2 && global1 <> global3 && global2 <> global3) && List.for_all (fun x -> List.mem x mem_safety_props) [global1; global2; global3] then
       MemorySafety
       (* if global = "valid-free" then
       ValidFree

From 1384f733d812996399648b4a846389fcbac29afb Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 09:57:38 +0200
Subject: [PATCH 021/104] Add support for SV-COMP's valid-memcleanup property

---
 src/autoTune.ml                |  1 +
 src/framework/analysisState.ml |  3 +++
 src/util/analysisStateUtil.ml  |  4 +++-
 src/witness/svcomp.ml          |  1 +
 src/witness/svcompSpec.ml      | 13 +++++++++++--
 src/witness/witness.ml         | 30 ++++++++++++++++++++++++++++++
 6 files changed, 49 insertions(+), 3 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 9e3508ccd2..ac7c150546 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -227,6 +227,7 @@ let focusOnSpecification () =
   | ValidDeref
   | ValidMemtrack -> ()
   | MemorySafety -> () (* TODO: This is here for now just to complete the pattern match *)
+  | ValidMemcleanup -> ()
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml
index ca619d4dfb..1416f99f69 100644
--- a/src/framework/analysisState.ml
+++ b/src/framework/analysisState.ml
@@ -16,6 +16,9 @@ let svcomp_may_invalid_deref = ref false
 (** Whether an invalid memtrack happened *)
 let svcomp_may_invalid_memtrack = ref false
 
+(** Whether an invalid memcleanup happened *)
+let svcomp_may_invalid_memcleanup = ref false
+
 (** A hack to see if we are currently doing global inits *)
 let global_initialization = ref false
 
diff --git a/src/util/analysisStateUtil.ml b/src/util/analysisStateUtil.ml
index 25914f8c8e..a34be33f18 100644
--- a/src/util/analysisStateUtil.ml
+++ b/src/util/analysisStateUtil.ml
@@ -2,10 +2,12 @@ type mem_safety_violation =
   | InvalidFree
   | InvalidDeref
   | InvalidMemTrack
+  | InvalidMemcleanup
 
 let set_mem_safety_flag violation_type =
   if !AnalysisState.postsolving then
     match violation_type with
     | InvalidFree -> AnalysisState.svcomp_may_invalid_free := true
     | InvalidDeref -> AnalysisState.svcomp_may_invalid_deref := true
-    | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true
\ No newline at end of file
+    | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true
+    | InvalidMemcleanup -> AnalysisState.svcomp_may_invalid_memcleanup := true
\ No newline at end of file
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 15d41c0210..22543d48a9 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -56,6 +56,7 @@ struct
         | ValidDeref -> "valid-deref"
         | ValidMemtrack -> "valid-memtrack"
         | MemorySafety -> "memory-safety" (* TODO: Currently here only to complete the pattern match *)
+        | ValidMemcleanup -> "valid-memcleanup"
       in
       "false(" ^ result_spec ^ ")"
     | Unknown -> "unknown"
diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index fbe206dabb..25a9f522bc 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -10,10 +10,12 @@ type t =
   | ValidDeref
   | ValidMemtrack
   | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
+  | ValidMemcleanup
 
 let of_string s =
   let s = String.strip s in
-  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp_multiple = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp_single = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
   if Str.string_match regexp_negated s 0 then
     let global_not = Str.matched_group 1 s in
@@ -28,7 +30,7 @@ let of_string s =
         UnreachCall f
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
-  else if Str.string_match regexp s 0 then
+  else if Str.string_match regexp_multiple s 0 then
     let global1 = Str.matched_group 1 s in
     let global2 = Str.matched_group 2 s in
     let global3 = Str.matched_group 3 s in
@@ -43,6 +45,12 @@ let of_string s =
           ValidMemtrack *)
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
+  else if Str.string_match regexp_single s 0 then
+    let global = Str.matched_group 1 s in
+    if global = "valid-memcleanup" then
+      ValidMemcleanup
+    else
+      failwith "Svcomp.Specification.of_string: unknown global expression"
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
@@ -72,5 +80,6 @@ let to_string spec =
     | ValidDeref -> "valid-deref", false
     | ValidMemtrack -> "valid-memtrack", false
     | MemorySafety -> "memory-safety", false (* TODO: That's false, it's currently here just to complete the pattern match *)
+    | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 17dd14472e..35d932210d 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -625,6 +625,36 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
+    | ValidMemcleanup ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_memcleanup then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
 
 
   let write entrystates =

From 4e70422c2c305de6408ef68177dddb1f3c9e9833 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 09:59:08 +0200
Subject: [PATCH 022/104] Set SV-COMP global flag for invalid-memcleanup

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

diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index eb38b97a1c..dbaa2d69fc 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -22,6 +22,7 @@ struct
   let warn_for_multi_threaded ctx =
     if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then (
       set_mem_safety_flag InvalidMemTrack;
+      set_mem_safety_flag InvalidMemcleanup;
       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"
     )
 
@@ -31,9 +32,11 @@ struct
       match assert_exp_imprecise, exp with
       | true, Some exp ->
         set_mem_safety_flag InvalidMemTrack;
+        set_mem_safety_flag InvalidMemcleanup;
         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
       | _ ->
         set_mem_safety_flag InvalidMemTrack;
+        set_mem_safety_flag InvalidMemcleanup;
         M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
 
   (* TRANSFER FUNCTIONS *)

From 00cc9b541ae6e6270906c16cbba94498692ab6f3 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 10:58:45 +0200
Subject: [PATCH 023/104] Enable memory safety analyses in autoTune

---
 src/autoTune.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index ac7c150546..f73a71ed40 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -223,11 +223,18 @@ let focusOnSpecification () =
     let uafAna = ["useAfterFree"] in
     print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
     enableAnalyses uafAna
-  (* TODO: Finish these two below later *)
-  | ValidDeref
-  | ValidMemtrack -> ()
-  | MemorySafety -> () (* TODO: This is here for now just to complete the pattern match *)
-  | ValidMemcleanup -> ()
+  | ValidDeref -> (* Enable the memOutOfBounds analysis *)
+    let memOobAna = ["memOutOfBounds"] in
+    print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
+    enableAnalyses memOobAna
+  | ValidMemtrack
+  | ValidMemcleanup -> (* Enable the memLeak analysis *)
+    let memLeakAna = ["memLeak"] in
+    print_endline @@ "Specification: ValidDeref and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
+    enableAnalyses memLeakAna
+  | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
+    let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
+    enableAnalyses memSafetyAnas
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound

From 2c8e927f4e5f88b0a4eb003da6fd24ac55a0e004 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Mon, 2 Oct 2023 10:59:36 +0200
Subject: [PATCH 024/104] Rename UAF tests from number 78 to 74

---
 .../{78-use_after_free => 74-use_after_free}/01-simple-uaf.c      | 0
 .../{78-use_after_free => 74-use_after_free}/02-conditional-uaf.c | 0
 .../{78-use_after_free => 74-use_after_free}/03-nested-ptr-uaf.c  | 0
 .../04-function-call-uaf.c                                        | 0
 .../05-uaf-free-in-wrapper-fun.c                                  | 0
 .../{78-use_after_free => 74-use_after_free}/06-uaf-struct.c      | 0
 .../{78-use_after_free => 74-use_after_free}/07-itc-double-free.c | 0
 .../08-itc-no-double-free.c                                       | 0
 .../{78-use_after_free => 74-use_after_free}/09-juliet-uaf.c      | 0
 .../10-juliet-double-free.c                                       | 0
 .../11-wrapper-funs-uaf.c                                         | 0
 .../12-multi-threaded-uaf.c                                       | 0
 .../13-multi-threaded-uaf-with-joined-thread.c                    | 0
 .../{78-use_after_free => 74-use_after_free}/14-alloca-uaf.c      | 0
 14 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/01-simple-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/02-conditional-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/03-nested-ptr-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/04-function-call-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/05-uaf-free-in-wrapper-fun.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/06-uaf-struct.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/07-itc-double-free.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/08-itc-no-double-free.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/09-juliet-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/10-juliet-double-free.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/11-wrapper-funs-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/12-multi-threaded-uaf.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/13-multi-threaded-uaf-with-joined-thread.c (100%)
 rename tests/regression/{78-use_after_free => 74-use_after_free}/14-alloca-uaf.c (100%)

diff --git a/tests/regression/78-use_after_free/01-simple-uaf.c b/tests/regression/74-use_after_free/01-simple-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/01-simple-uaf.c
rename to tests/regression/74-use_after_free/01-simple-uaf.c
diff --git a/tests/regression/78-use_after_free/02-conditional-uaf.c b/tests/regression/74-use_after_free/02-conditional-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/02-conditional-uaf.c
rename to tests/regression/74-use_after_free/02-conditional-uaf.c
diff --git a/tests/regression/78-use_after_free/03-nested-ptr-uaf.c b/tests/regression/74-use_after_free/03-nested-ptr-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/03-nested-ptr-uaf.c
rename to tests/regression/74-use_after_free/03-nested-ptr-uaf.c
diff --git a/tests/regression/78-use_after_free/04-function-call-uaf.c b/tests/regression/74-use_after_free/04-function-call-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/04-function-call-uaf.c
rename to tests/regression/74-use_after_free/04-function-call-uaf.c
diff --git a/tests/regression/78-use_after_free/05-uaf-free-in-wrapper-fun.c b/tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c
similarity index 100%
rename from tests/regression/78-use_after_free/05-uaf-free-in-wrapper-fun.c
rename to tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c
diff --git a/tests/regression/78-use_after_free/06-uaf-struct.c b/tests/regression/74-use_after_free/06-uaf-struct.c
similarity index 100%
rename from tests/regression/78-use_after_free/06-uaf-struct.c
rename to tests/regression/74-use_after_free/06-uaf-struct.c
diff --git a/tests/regression/78-use_after_free/07-itc-double-free.c b/tests/regression/74-use_after_free/07-itc-double-free.c
similarity index 100%
rename from tests/regression/78-use_after_free/07-itc-double-free.c
rename to tests/regression/74-use_after_free/07-itc-double-free.c
diff --git a/tests/regression/78-use_after_free/08-itc-no-double-free.c b/tests/regression/74-use_after_free/08-itc-no-double-free.c
similarity index 100%
rename from tests/regression/78-use_after_free/08-itc-no-double-free.c
rename to tests/regression/74-use_after_free/08-itc-no-double-free.c
diff --git a/tests/regression/78-use_after_free/09-juliet-uaf.c b/tests/regression/74-use_after_free/09-juliet-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/09-juliet-uaf.c
rename to tests/regression/74-use_after_free/09-juliet-uaf.c
diff --git a/tests/regression/78-use_after_free/10-juliet-double-free.c b/tests/regression/74-use_after_free/10-juliet-double-free.c
similarity index 100%
rename from tests/regression/78-use_after_free/10-juliet-double-free.c
rename to tests/regression/74-use_after_free/10-juliet-double-free.c
diff --git a/tests/regression/78-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/11-wrapper-funs-uaf.c
rename to tests/regression/74-use_after_free/11-wrapper-funs-uaf.c
diff --git a/tests/regression/78-use_after_free/12-multi-threaded-uaf.c b/tests/regression/74-use_after_free/12-multi-threaded-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/12-multi-threaded-uaf.c
rename to tests/regression/74-use_after_free/12-multi-threaded-uaf.c
diff --git a/tests/regression/78-use_after_free/13-multi-threaded-uaf-with-joined-thread.c b/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
similarity index 100%
rename from tests/regression/78-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
rename to tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
diff --git a/tests/regression/78-use_after_free/14-alloca-uaf.c b/tests/regression/74-use_after_free/14-alloca-uaf.c
similarity index 100%
rename from tests/regression/78-use_after_free/14-alloca-uaf.c
rename to tests/regression/74-use_after_free/14-alloca-uaf.c

From f87285462b6cdcff1a2081b0d80b266ce248a358 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 12:57:44 +0300
Subject: [PATCH 025/104] Fix print for valid-memtrack and valid-memcleanup in
 `autoTune.ml`

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 src/autoTune.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index f73a71ed40..e093c63f08 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -230,7 +230,7 @@ let focusOnSpecification () =
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in
-    print_endline @@ "Specification: ValidDeref and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
+    print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
     let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in

From edaef4230d6db75def47f41b4a748c9cbd5aa83d Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 12:02:01 +0200
Subject: [PATCH 026/104] Set `ana.malloc.unique_address_count` to `1` when
 activating memLeak analysis

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index e093c63f08..0441fe0b4f 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -230,6 +230,8 @@ let focusOnSpecification () =
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in
+    print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
+    set_int "ana.malloc.unique_address_count" 1;
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)

From 7f0b43ccf1db2d6c3bec95ce1ea759dff84e4fba Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 12:09:00 +0200
Subject: [PATCH 027/104] Improve some `AnalysisState` global flag comments

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

diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml
index 1416f99f69..05a93741f8 100644
--- a/src/framework/analysisState.ml
+++ b/src/framework/analysisState.ml
@@ -13,10 +13,10 @@ let svcomp_may_invalid_free = ref false
 (** Whether an invalid pointer dereference happened *)
 let svcomp_may_invalid_deref = ref false
 
-(** Whether an invalid memtrack happened *)
+(** Whether a memory leak occurred and there's no reference to the leaked memory *)
 let svcomp_may_invalid_memtrack = ref false
 
-(** Whether an invalid memcleanup happened *)
+(** Whether a memory leak occurred *)
 let svcomp_may_invalid_memcleanup = ref false
 
 (** A hack to see if we are currently doing global inits *)

From a975702f700511c3c1f0b71979502462192d9bc2 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 12:25:33 +0200
Subject: [PATCH 028/104] Clean up some commented out code

---
 src/witness/svcompSpec.ml |  6 ---
 src/witness/witness.ml    | 93 ++-------------------------------------
 2 files changed, 3 insertions(+), 96 deletions(-)

diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index 25a9f522bc..4a3da23d9b 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -37,12 +37,6 @@ let of_string s =
     let mem_safety_props = ["valid-free"; "valid-deref"; "valid-memtrack";] in
     if (global1 <> global2 && global1 <> global3 && global2 <> global3) && List.for_all (fun x -> List.mem x mem_safety_props) [global1; global2; global3] then
       MemorySafety
-      (* if global = "valid-free" then
-      ValidFree
-    else if global = "valid-deref" then
-      ValidDeref
-    else if global = "valid-memtrack" then
-          ValidMemtrack *)
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
   else if Str.string_match regexp_single s 0 then
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 35d932210d..a28f69f76a 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -505,96 +505,9 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree (*->*)
-    (* let module TrivialArg =
-      struct
-        include Arg
-        let next _ = []
-      end
-      in
-      if not !AnalysisState.svcomp_may_invalid_free then (
-        let module TaskResult =
-        struct
-          module Arg = Arg
-          let result = Result.True
-          let invariant _ = Invariant.none
-          let is_violation _ = false
-          let is_sink _ = false
-        end
-        in
-        (module TaskResult:WitnessTaskResult)
-      ) else (
-        let module TaskResult =
-        struct
-          module Arg = TrivialArg
-          let result = Result.Unknown
-          let invariant _ = Invariant.none
-          let is_violation _ = false
-          let is_sink _ = false
-        end
-        in
-        (module TaskResult:WitnessTaskResult)
-        ) *)
-    | ValidDeref (*->*)
-    (* let module TrivialArg =
-      struct
-        include Arg
-        let next _ = []
-      end
-      in
-      if not !AnalysisState.svcomp_may_invalid_deref then (
-        let module TaskResult =
-        struct
-          module Arg = Arg
-          let result = Result.True
-          let invariant _ = Invariant.none
-          let is_violation _ = false
-          let is_sink _ = false
-        end
-        in
-        (module TaskResult:WitnessTaskResult)
-      ) else (
-        let module TaskResult =
-        struct
-          module Arg = TrivialArg
-          let result = Result.Unknown
-          let invariant _ = Invariant.none
-          let is_violation _ = false
-          let is_sink _ = false
-        end
-        in
-        (module TaskResult:WitnessTaskResult)
-        ) *)
-    | ValidMemtrack (*->*)
-    (* let module TrivialArg =
-      struct
-        include Arg
-        let next _ = []
-      end
-      in
-      if not !AnalysisState.svcomp_may_invalid_memtrack then (
-        let module TaskResult =
-        struct
-          module Arg = Arg
-          let result = Result.True
-          let invariant _ = Invariant.none
-          let is_violation _ = false
-          let is_sink _ = false
-        end
-        in
-        (module TaskResult:WitnessTaskResult)
-        ) else (
-        let module TaskResult =
-        struct
-          module Arg = TrivialArg
-          let result = Result.Unknown
-          let invariant _ = Invariant.none
-          let is_violation _ = false
-          let is_sink _ = false
-        end
-        in
-        (module TaskResult:WitnessTaskResult)
-        ) *)
+    | ValidFree
+    | ValidDeref
+    | ValidMemtrack
     | MemorySafety ->
       let module TrivialArg =
       struct

From b26010ac042143b4cdeb806b2a35b67054db1d76 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 12:31:31 +0200
Subject: [PATCH 029/104] Set `ana.malloc.unique_address_count` to `1` only if
 it's not already set to a value >= 1

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 0441fe0b4f..4912d645ce 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -230,8 +230,10 @@ let focusOnSpecification () =
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in
-    print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
-    set_int "ana.malloc.unique_address_count" 1;
+    if (get_int "ana.malloc.unique_address_count") < 1 then (
+      print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
+      set_int "ana.malloc.unique_address_count" 1;
+    );
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)

From 89d68af6d7c68a647e13dd77e876580dbc8e71b1 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 12:35:30 +0200
Subject: [PATCH 030/104] Add a valid-memcleanup.prp file

---
 tests/sv-comp/valid-memcleanup.prp | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 tests/sv-comp/valid-memcleanup.prp

diff --git a/tests/sv-comp/valid-memcleanup.prp b/tests/sv-comp/valid-memcleanup.prp
new file mode 100644
index 0000000000..778c49e5dc
--- /dev/null
+++ b/tests/sv-comp/valid-memcleanup.prp
@@ -0,0 +1,2 @@
+CHECK( init(main()), LTL(G valid-memcleanup) )
+

From 171ba57b315044c20252fbff625a652c0f2d328f Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 15:13:00 +0200
Subject: [PATCH 031/104] Comment out reachability filter in useAfterFree's
 `enter`

---
 src/analyses/useAfterFree.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index a28591e273..805bf1792c 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -182,7 +182,8 @@ struct
   let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let caller_state = ctx.local in
     List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args;
-    if AllocaVars.is_empty (fst caller_state) && HeapVars.is_empty (snd caller_state) then
+    [(caller_state, caller_state)]
+  (* if AllocaVars.is_empty (fst caller_state) && HeapVars.is_empty (snd caller_state) then
       [caller_state, caller_state]
     else (
       let reachable_from_args = List.fold_left (fun ad arg -> Queries.AD.join ad (ctx.ask (ReachableFrom arg))) (Queries.AD.empty ()) args in
@@ -192,7 +193,7 @@ struct
         let reachable_vars = Queries.AD.to_var_may reachable_from_args in
         let callee_state = (AllocaVars.empty (), HeapVars.filter (fun var -> List.mem var reachable_vars) (snd caller_state)) in (* TODO: use AD.mem directly *)
         [caller_state, callee_state]
-    )
+        ) *)
 
   let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t =
     let (caller_stack_state, caller_heap_state) = ctx.local in

From 4a1c038b5bd32674b8dff3bd9499d4a6ddbb2f85 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 15:25:31 +0200
Subject: [PATCH 032/104] Fix wrong callee_state in enter

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

diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 805bf1792c..521f17d97f 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -182,7 +182,7 @@ struct
   let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let caller_state = ctx.local in
     List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args;
-    [(caller_state, caller_state)]
+    [caller_state, (AllocaVars.empty (), snd caller_state)]
   (* if AllocaVars.is_empty (fst caller_state) && HeapVars.is_empty (snd caller_state) then
       [caller_state, caller_state]
     else (

From bb2091e5038a437c23db3c8711d38f19a301ef05 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 15:25:45 +0200
Subject: [PATCH 033/104] Add test case for UAF in callee through a global var

---
 .../15-juliet-uaf-global-var.c                | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/regression/74-use_after_free/15-juliet-uaf-global-var.c

diff --git a/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c b/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c
new file mode 100644
index 0000000000..9cb3b2b29a
--- /dev/null
+++ b/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c
@@ -0,0 +1,24 @@
+//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+
+int *global;
+
+void other(void)
+{
+  int *data = global;
+  free((void *)data);
+  return;
+}
+
+int main(int argc, char **argv)
+{
+    int *data = (int *)malloc(400UL);
+    free((void *)data);
+
+    global = data;
+    other();
+
+    return 0;
+}
\ No newline at end of file

From fb4ad24d4f71f93181c3b908398bc785c5c32dfe Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 16:32:48 +0200
Subject: [PATCH 034/104] Fix typo for warning about top address offsets

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

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index db86a63414..ca2cf82116 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -205,7 +205,7 @@ struct
                 set_mem_safety_flag InvalidDeref;
                 M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr
               ) else if VDQ.AD.exists (function
-                  | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o
+                  | Addr (_, o) -> ID.is_top_of (Cilfacade.ptrdiff_ikind ()) (offs_to_idx t o)
                   | _ -> false
                 ) a then (
                 set_mem_safety_flag InvalidDeref;

From 9d64db11a69abf60b0c777ee591860416c49666d Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 16:33:09 +0200
Subject: [PATCH 035/104] Add test case with invalid deref in complex loop

---
 .../regression/77-mem-oob/10-oob-two-loops.c  | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 tests/regression/77-mem-oob/10-oob-two-loops.c

diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/77-mem-oob/10-oob-two-loops.c
new file mode 100644
index 0000000000..2661f3dff7
--- /dev/null
+++ b/tests/regression/77-mem-oob/10-oob-two-loops.c
@@ -0,0 +1,20 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+int main() {
+	int *p = malloc(1048 * sizeof(int));
+
+    for (int i = 0; i < 1048; ++i) {
+		p[i] = __VERIFIER_nondet_int(); //NOWARN
+	}
+
+	int *q = p;
+
+	while (*q >= 0 && q < p + 1048 * sizeof(int)) { //WARN
+		if (__VERIFIER_nondet_int()) {
+			q++;
+		} else {
+			(*q)--; //WARN
+		}
+	}
+	free(p);
+	return 0;
+}

From 1afac024c34280a8c1b6bfbeae254654800d5919 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 16:39:30 +0200
Subject: [PATCH 036/104] Disable info messages which confuse `make test` in
 77/10

---
 tests/regression/77-mem-oob/10-oob-two-loops.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/77-mem-oob/10-oob-two-loops.c
index 2661f3dff7..6737a212bf 100644
--- a/tests/regression/77-mem-oob/10-oob-two-loops.c
+++ b/tests/regression/77-mem-oob/10-oob-two-loops.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
 int main() {
 	int *p = malloc(1048 * sizeof(int));
 

From f5c197e119e44fa997022daebaaae98d8e07ecf0 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 17:28:47 +0200
Subject: [PATCH 037/104] Add option for enabling the marking of variables as
 pulled out of scope

---
 src/util/cilfacade.ml        | 4 +++-
 src/util/options.schema.json | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index eb7330aa19..32b6627319 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -51,7 +51,9 @@ let init () =
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
   print_CIL_Input := true;
-  Cabs2cil.allowDuplication := false
+  Cabs2cil.allowDuplication := false;
+  if get_bool "cil.addNestedScopeAttr" then
+    Cabs2cil.addNestedScopeAttr := true
 
 let current_file = ref dummyFile
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 1b9c7d3fd5..400dde06dc 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -288,6 +288,12 @@
           "type": "boolean",
           "description": "Indicates whether gnu89 semantic should be used for inline functions.",
           "default": false
+        },
+        "addNestedScopeAttr": {
+          "title": "cil.addNestedScopeAttr",
+          "type": "boolean",
+          "description": "Indicates whether variables that CIL pulls out of their scope should be marked.",
+          "default": false
         }
       },
       "additionalProperties": false

From 003b8148f3cb5035f083ee8c8e3ab339b3d9538e Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 17:29:17 +0200
Subject: [PATCH 038/104] Warn for accesses to variables pulled out of scope

---
 src/analyses/memOutOfBounds.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index ca2cf82116..9db6e58e5f 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -228,6 +228,7 @@ struct
       ID.top_of @@ Cilfacade.ptrdiff_ikind ()
 
   and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval =
+    check_lval_out_of_scope_access lval;
     (* If the lval does not contain a pointer or if it does contain a pointer, but only points to string addresses, then no need to WARN *)
     if (not @@ lval_contains_a_ptr lval) || ptr_only_has_str_addr ctx (Lval lval) then ()
     else
@@ -246,6 +247,15 @@ struct
           | _ -> check_exp_for_oob_access ctx ~is_implicitly_derefed e
         end
 
+  and check_lval_out_of_scope_access lval =
+    match lval with
+    | (Var v, _) ->
+      if hasAttribute "goblint_cil_nested" v.vattr then (
+        set_mem_safety_flag InvalidDeref;
+        M.warn "Lvalue %a is potentially accessed out-of-scope. Invalid memory access may occur" d_lval lval
+      )
+    | _ -> ()
+
   and check_no_binop_deref ctx lval_exp =
     check_unknown_addr_deref ctx lval_exp;
     let behavior = Undefined MemoryOutOfBoundsAccess in

From ac7dd717c0dc8f353130c1395dc0f7910aaf8f24 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 17:29:44 +0200
Subject: [PATCH 039/104] Automatically set `cil.addNestedScopeAttr` in
 autoTune when running `memOutOfBounds`

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 4912d645ce..4e0080d0bd 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -225,6 +225,8 @@ let focusOnSpecification () =
     enableAnalyses uafAna
   | ValidDeref -> (* Enable the memOutOfBounds analysis *)
     let memOobAna = ["memOutOfBounds"] in
+    print_endline "Setting \"cil.addNestedScopeAttr\" to true";
+    set_bool "cil.addNestedScopeAttr" true;
     print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
     enableAnalyses memOobAna
   | ValidMemtrack

From c95a846617c7a73c86d5a2e4655b5e0f16d4f32e Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 17:59:18 +0200
Subject: [PATCH 040/104] Bump goblint-cil

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

diff --git a/goblint.opam b/goblint.opam
index 661222805b..88289820c1 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -74,12 +74,12 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
+pin-depends: [
   # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index bb59c41dd1..31acfdd4ea 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -122,6 +122,9 @@ build: [
 ]
 dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
+pin-depends: [
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
+]
 conflicts: [
   "result" {< "1.5"}
 ]
diff --git a/goblint.opam.template b/goblint.opam.template
index 6259c4d498..3476f5befe 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,12 +1,12 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
+pin-depends: [
   # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

From c9a846b6a74f1dd37f53d15d9909adb291ec82da Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 3 Oct 2023 18:48:01 +0200
Subject: [PATCH 041/104] set also for meta property

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 4e0080d0bd..10c9570d46 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -239,8 +239,10 @@ let focusOnSpecification () =
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
-    let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
-    enableAnalyses memSafetyAnas
+    (print_endline "Setting \"cil.addNestedScopeAttr\" to true";
+     set_bool "cil.addNestedScopeAttr" true;
+     let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
+     enableAnalyses memSafetyAnas)
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound

From 9efae6f8bef52e96d99052443f6a6a31a50f4dca Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 23:50:32 +0200
Subject: [PATCH 042/104] Fix address offset calculation in `memOutOfBounds`

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

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 9db6e58e5f..aadf433a6e 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -211,11 +211,16 @@ struct
                 set_mem_safety_flag InvalidDeref;
                 M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr
               );
-              (* Offset should be the same for all elements in the points-to set *)
-              (* Hence, we can just pick one element and obtain its offset *)
-              begin match VDQ.AD.choose a with
-                | Addr (_, o) -> offs_to_idx t o
-                | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
+              (* Get the address offsets of all points-to set elements *)
+              let addr_offsets =
+                VDQ.AD.filter (function Addr (v, o) -> true | _ -> false) a
+                |> VDQ.AD.to_mval
+                |> List.map (fun (_, o) -> offs_to_idx t o)
+              in
+              begin match addr_offsets with
+                | [] -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+                | [x] -> x
+                | x::xs -> List.fold_left ID.join x xs
               end
           end
         | None ->

From dcc3d5c3c608414092171f55fda99ebcd18d29c4 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 23:53:12 +0200
Subject: [PATCH 043/104] Adapt 77/10 test case to correctly account for
 address offsets

---
 tests/regression/77-mem-oob/10-oob-two-loops.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/77-mem-oob/10-oob-two-loops.c
index 6737a212bf..5208da5a0b 100644
--- a/tests/regression/77-mem-oob/10-oob-two-loops.c
+++ b/tests/regression/77-mem-oob/10-oob-two-loops.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info --set sem.int.signed_overflow assume_none
 int main() {
 	int *p = malloc(1048 * sizeof(int));
 

From a64e9c37e0b12eaa767e5f43f28b952c41ffa318 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 23:53:36 +0200
Subject: [PATCH 044/104] Add further test case to check address offset
 calculation in `memOutOfBounds`

---
 .../77-mem-oob/11-address-offset-oob.c           | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 tests/regression/77-mem-oob/11-address-offset-oob.c

diff --git a/tests/regression/77-mem-oob/11-address-offset-oob.c b/tests/regression/77-mem-oob/11-address-offset-oob.c
new file mode 100644
index 0000000000..ba01a12873
--- /dev/null
+++ b/tests/regression/77-mem-oob/11-address-offset-oob.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info --set sem.int.signed_overflow assume_none
+int main() {
+    int *p = malloc(2 * sizeof(int));
+    int *q = p;
+    int x;
+
+    if (x) {
+        q++;
+        q++;
+        q++;
+        x = *q;  //WARN
+    }
+
+    x = *q;  //WARN
+    return 0;
+}

From 44476ce76e283c8adbdcb445c1799186cc1c3320 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Tue, 3 Oct 2023 23:56:46 +0200
Subject: [PATCH 045/104] Set `ana.malloc.unique_address_count` for
 `MemorySafety` as well

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 10c9570d46..822195b1f6 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -241,6 +241,10 @@ let focusOnSpecification () =
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
     (print_endline "Setting \"cil.addNestedScopeAttr\" to true";
      set_bool "cil.addNestedScopeAttr" true;
+     if (get_int "ana.malloc.unique_address_count") < 1 then (
+       print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
+       set_int "ana.malloc.unique_address_count" 1;
+     );
      let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
      enableAnalyses memSafetyAnas)
 

From e052544e9d225c6292ecce05a0468f3dad7b5f31 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 11:14:50 +0200
Subject: [PATCH 046/104] Move `cil.addNestedScopeAttr` setting to
 `init_options`

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

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 8eaef280c6..6ca9023324 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -40,7 +40,9 @@ let is_first_field x = match x.fcomp.cfields with
 let init_options () =
   Mergecil.merge_inlines := get_bool "cil.merge.inlines";
   Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
-  Cil.gnu89inline := get_bool "cil.gnu89inline"
+  Cil.gnu89inline := get_bool "cil.gnu89inline";
+  if get_bool "cil.addNestedScopeAttr" = true then
+    Cabs2cil.addNestedScopeAttr := true
 
 let init () =
   initCIL ();
@@ -51,9 +53,7 @@ let init () =
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
   print_CIL_Input := true;
-  Cabs2cil.allowDuplication := false;
-  if get_bool "cil.addNestedScopeAttr" then
-    Cabs2cil.addNestedScopeAttr := true
+  Cabs2cil.allowDuplication := false
 
 let current_file = ref dummyFile
 

From 33414703562868d35f974bc2201238733959874c Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 11:36:10 +0200
Subject: [PATCH 047/104] Try with `cil.addNestedScopeAttr` always set to
 `true`

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

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 6ca9023324..7009512adf 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -41,8 +41,8 @@ let init_options () =
   Mergecil.merge_inlines := get_bool "cil.merge.inlines";
   Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
   Cil.gnu89inline := get_bool "cil.gnu89inline";
-  if get_bool "cil.addNestedScopeAttr" = true then
-    Cabs2cil.addNestedScopeAttr := true
+  (* if get_bool "cil.addNestedScopeAttr" = true then *)
+  Cabs2cil.addNestedScopeAttr := true
 
 let init () =
   initCIL ();

From 1211a9fe95fb881e8d53a7ab474498c31d675b7e Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 12:25:10 +0200
Subject: [PATCH 048/104] Use rand() in 77/10

---
 tests/regression/77-mem-oob/10-oob-two-loops.c | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/77-mem-oob/10-oob-two-loops.c
index 5208da5a0b..303aac242e 100644
--- a/tests/regression/77-mem-oob/10-oob-two-loops.c
+++ b/tests/regression/77-mem-oob/10-oob-two-loops.c
@@ -1,15 +1,17 @@
 // PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info --set sem.int.signed_overflow assume_none
+#include <stdlib.h>
+
 int main() {
 	int *p = malloc(1048 * sizeof(int));
 
     for (int i = 0; i < 1048; ++i) {
-		p[i] = __VERIFIER_nondet_int(); //NOWARN
+		p[i] = rand(); //NOWARN
 	}
 
 	int *q = p;
 
 	while (*q >= 0 && q < p + 1048 * sizeof(int)) { //WARN
-		if (__VERIFIER_nondet_int()) {
+		if (rand()) {
 			q++;
 		} else {
 			(*q)--; //WARN

From 20396754a27385fdc788557ef30704da339ae8cc Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 12:45:14 +0200
Subject: [PATCH 049/104] Activate `cil.addNestedScopeAttr` in cilfacade only
 conditionally

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

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 7009512adf..7ac3e29ee0 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -41,8 +41,8 @@ let init_options () =
   Mergecil.merge_inlines := get_bool "cil.merge.inlines";
   Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
   Cil.gnu89inline := get_bool "cil.gnu89inline";
-  (* if get_bool "cil.addNestedScopeAttr" = true then *)
-  Cabs2cil.addNestedScopeAttr := true
+  if get_bool "cil.addNestedScopeAttr" then
+    Cabs2cil.addNestedScopeAttr := true
 
 let init () =
   initCIL ();

From fb4979b567d4664c9012d3d98a9a32ba2f0b39d9 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 12:46:11 +0200
Subject: [PATCH 050/104] Activate SV-COMP memory-safety-related options before
 CIL has completely parsed the program

---
 src/autoTune.ml | 21 +++++++++++++--------
 src/goblint.ml  |  2 ++
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 822195b1f6..186d930189 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -210,15 +210,8 @@ let activateLongjmpAnalysesWhenRequired () =
     enableAnalyses longjmpAnalyses;
   )
 
-let focusOnSpecification () =
+let focusOnMemSafetySpecification () =
   match Svcomp.Specification.of_option () with
-  | UnreachCall s -> ()
-  | NoDataRace -> (*enable all thread analyses*)
-    print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\"";
-    enableAnalyses notNeccessaryThreadAnalyses;
-  | NoOverflow -> (*We focus on integer analysis*)
-    set_bool "ana.int.def_exc" true;
-    set_bool "ana.int.interval" true
   | ValidFree -> (* Enable the useAfterFree analysis *)
     let uafAna = ["useAfterFree"] in
     print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
@@ -247,6 +240,18 @@ let focusOnSpecification () =
      );
      let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
      enableAnalyses memSafetyAnas)
+  | _ -> ()
+
+let focusOnSpecification () =
+  match Svcomp.Specification.of_option () with
+  | UnreachCall s -> ()
+  | NoDataRace -> (*enable all thread analyses*)
+    print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\"";
+    enableAnalyses notNeccessaryThreadAnalyses;
+  | NoOverflow -> (*We focus on integer analysis*)
+    set_bool "ana.int.def_exc" true;
+    set_bool "ana.int.interval" true
+  | _ -> ()
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
diff --git a/src/goblint.ml b/src/goblint.ml
index 4ea3a3d242..45dae3a4c6 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -56,6 +56,8 @@ let main () =
         else
           None
       in
+      if AutoTune.isActivated "specification" && get_string "ana.specification" <> "" then
+        AutoTune.focusOnMemSafetySpecification ();
       (* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
       AutoTune.activateLongjmpAnalysesWhenRequired ();
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;

From 1eb7309b472c1392b1812fecf4adb1b2b756bb05 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 13:59:05 +0200
Subject: [PATCH 051/104] Fix again scoping check

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

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index aadf433a6e..655ed7d3f1 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -89,6 +89,10 @@ struct
         let pts_elems_to_sizes (addr: Queries.AD.elt) =
           begin match addr with
             | Addr (v, _) ->
+              if hasAttribute "goblint_cil_nested" v.vattr then (
+                set_mem_safety_flag InvalidDeref;
+                M.warn "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v
+              );
               begin match v.vtype with
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
@@ -233,7 +237,6 @@ struct
       ID.top_of @@ Cilfacade.ptrdiff_ikind ()
 
   and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval =
-    check_lval_out_of_scope_access lval;
     (* If the lval does not contain a pointer or if it does contain a pointer, but only points to string addresses, then no need to WARN *)
     if (not @@ lval_contains_a_ptr lval) || ptr_only_has_str_addr ctx (Lval lval) then ()
     else
@@ -252,15 +255,6 @@ struct
           | _ -> check_exp_for_oob_access ctx ~is_implicitly_derefed e
         end
 
-  and check_lval_out_of_scope_access lval =
-    match lval with
-    | (Var v, _) ->
-      if hasAttribute "goblint_cil_nested" v.vattr then (
-        set_mem_safety_flag InvalidDeref;
-        M.warn "Lvalue %a is potentially accessed out-of-scope. Invalid memory access may occur" d_lval lval
-      )
-    | _ -> ()
-
   and check_no_binop_deref ctx lval_exp =
     check_unknown_addr_deref ctx lval_exp;
     let behavior = Undefined MemoryOutOfBoundsAccess in

From 4a4b6abc6edd18d1487084131a4f3bc038fe526f Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 19:48:48 +0200
Subject: [PATCH 052/104] Fix conditional enabling of `cil.addNestedScopeAttr`

---
 src/goblint.ml     | 2 --
 src/maingoblint.ml | 2 ++
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/goblint.ml b/src/goblint.ml
index 45dae3a4c6..4ea3a3d242 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -56,8 +56,6 @@ let main () =
         else
           None
       in
-      if AutoTune.isActivated "specification" && get_string "ana.specification" <> "" then
-        AutoTune.focusOnMemSafetySpecification ();
       (* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
       AutoTune.activateLongjmpAnalysesWhenRequired ();
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 155faa0e76..0f061a3507 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -185,6 +185,8 @@ let handle_options () =
   check_arguments ();
   AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
+  if AutoTune.isActivated "specification" && get_string "ana.specification" <> "" then
+    AutoTune.focusOnMemSafetySpecification ();
   Cilfacade.init_options ();
   handle_flags ()
 

From 395c30db266591bc2e20b663274628278bb3b6f0 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 20:39:15 +0200
Subject: [PATCH 053/104] Warn for invalid deallocation when encountering
 invalid addresses

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 81bd29f8d0..a9457ca41b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2039,7 +2039,9 @@ struct
         AnalysisStateUtil.set_mem_safety_flag InvalidFree;
         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
+    | _ ->
+      AnalysisStateUtil.set_mem_safety_flag InvalidFree;
+      M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname
 
 
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =

From 055d9cc01b2fa8332c00e9011183d18cd2bf2fc6 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 20:39:39 +0200
Subject: [PATCH 054/104] Add invalid address test case for invalid
 deallocation

---
 .../10-invalid-dealloc-union.c                | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 tests/regression/75-invalid_dealloc/10-invalid-dealloc-union.c

diff --git a/tests/regression/75-invalid_dealloc/10-invalid-dealloc-union.c b/tests/regression/75-invalid_dealloc/10-invalid-dealloc-union.c
new file mode 100644
index 0000000000..be1eaa056d
--- /dev/null
+++ b/tests/regression/75-invalid_dealloc/10-invalid-dealloc-union.c
@@ -0,0 +1,42 @@
+extern void abort(void);
+#include <stdlib.h>
+
+extern int __VERIFIER_nondet_int(void);
+
+int main()
+{
+    union {
+        void *p0;
+
+        struct {
+            char c[2];
+            int  p1;
+            int  p2;
+        } str;
+
+    } data;
+
+    // alloc 37B on heap
+    data.p0 = malloc(37U);
+
+    // avoid introducing a memleak
+    void *ptr = data.p0;
+    
+    // this should be fine
+    if(__VERIFIER_nondet_int()) {
+      data.str.p2 = 20;
+    } else {
+      data.str.p2 = 30;
+    }
+    
+    if(25 > data.str.p2) {
+       // avoids memleak
+       data.str.c[1] = sizeof data.str.p1;
+    }
+
+    // invalid free()
+    free(data.p0);//WARN
+
+    free(ptr);//NOWARN
+    return 0;
+}

From 2c883eb32cc67f17a48bb4ff7aca73f5811a056b Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 21:58:30 +0200
Subject: [PATCH 055/104] Warn if lval contains an address with a non-local var

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a9457ca41b..a323e5f270 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1051,7 +1051,18 @@ struct
             else if AD.may_be_null adr then (
               AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
               M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer"
-            )
+            );
+            (* Warn if any of the addresses contains a non-local variable *)
+            AD.iter (function
+                | AD.Addr.Addr (v,o) ->
+                  if not @@ CPA.mem v st.cpa then (
+                    (* TODO: Not the smartest move to set the global flag within an iter *)
+                    (* TODO: We can resort to using AD.exists instead *)
+                    AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
+                    M.warn "lval %a points to non-local variable %a. Invalid pointer dereference may occur" d_lval lval CilType.Varinfo.pretty v
+                  )
+                | _ -> ()
+              ) adr
           );
           AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
         | _ ->

From 5cb10f61925e55932475e859569d496a630fee6a Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 22:09:51 +0200
Subject: [PATCH 056/104] Don't warn for non-local vars in address set if
 they're globals

---
 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 a323e5f270..a5b60e8cca 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1055,7 +1055,7 @@ struct
             (* Warn if any of the addresses contains a non-local variable *)
             AD.iter (function
                 | AD.Addr.Addr (v,o) ->
-                  if not @@ CPA.mem v st.cpa then (
+                  if not (CPA.mem v st.cpa) && not (is_global a v) then (
                     (* TODO: Not the smartest move to set the global flag within an iter *)
                     (* TODO: We can resort to using AD.exists instead *)
                     AnalysisStateUtil.set_mem_safety_flag InvalidDeref;

From ea4410d8d0939d93f5effa56fd51c9549c717641 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 22:10:11 +0200
Subject: [PATCH 057/104] Add test cases for invalid deref due to scoping

---
 .../01-scopes-no-static.c                     | 22 ++++++++
 .../02-scopes-global-var.c                    | 29 +++++++++++
 .../03-scopes-static.c                        | 52 +++++++++++++++++++
 3 files changed, 103 insertions(+)
 create mode 100644 tests/regression/78-invalid-deref-scopes/01-scopes-no-static.c
 create mode 100644 tests/regression/78-invalid-deref-scopes/02-scopes-global-var.c
 create mode 100644 tests/regression/78-invalid-deref-scopes/03-scopes-static.c

diff --git a/tests/regression/78-invalid-deref-scopes/01-scopes-no-static.c b/tests/regression/78-invalid-deref-scopes/01-scopes-no-static.c
new file mode 100644
index 0000000000..e0c4b47b73
--- /dev/null
+++ b/tests/regression/78-invalid-deref-scopes/01-scopes-no-static.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] memOutOfBounds
+// TODO: I haven't checked why, but we need memOutOfBounds for this case
+extern int printf ( const char * format, ... );
+
+int *foo2(void)
+{
+    int arr[1024];
+    arr[194] = 13;
+    return arr + 1;
+}
+
+int *foo(void)
+{
+    int arr[123];
+    return foo2();
+}
+
+int main(void) {
+    int *a = foo();
+    printf("%d\n", *a);//WARN
+    return 0;
+}
diff --git a/tests/regression/78-invalid-deref-scopes/02-scopes-global-var.c b/tests/regression/78-invalid-deref-scopes/02-scopes-global-var.c
new file mode 100644
index 0000000000..9491e1c574
--- /dev/null
+++ b/tests/regression/78-invalid-deref-scopes/02-scopes-global-var.c
@@ -0,0 +1,29 @@
+int array[10];
+
+// function returns array of numbers
+int* getNumbers(void) {
+    for (int i = 0; i < 10; ++i) {
+       array[i] = i;//NOWARN
+    }
+
+    return array;
+}
+
+int* getNumbers2(void) {
+    int* numbers = getNumbers();
+    // numbers2 is local
+    int numbers2[10];
+
+    for (int i = 0; i < 10; ++i) {
+        numbers2[i] = numbers[i];//NOWARN
+    }
+
+    return numbers2;
+}
+
+int main(void) {
+   int *numbers = getNumbers2();
+   numbers[0] = 100;//WARN
+
+   return 0;
+}
diff --git a/tests/regression/78-invalid-deref-scopes/03-scopes-static.c b/tests/regression/78-invalid-deref-scopes/03-scopes-static.c
new file mode 100644
index 0000000000..c13b665c84
--- /dev/null
+++ b/tests/regression/78-invalid-deref-scopes/03-scopes-static.c
@@ -0,0 +1,52 @@
+extern int printf (const char* format, ...);
+
+// function returns array of numbers
+int* getNumbers() {
+
+    static int array[10];
+
+    for (int i = 0; i < 10; ++i) {
+       array[i] = i;//NOWARN
+    }
+
+    return array;
+}
+
+int* getNumbers2() {
+    int* numbers = getNumbers();
+    static int numbers2[10];
+    for (int i = 0; i < 10; ++i) {
+        numbers2[i] = numbers[i];//NOWARN
+    }
+    return numbers2;
+}
+
+int* getNumbers3() {
+    int* numbers = getNumbers2();
+    int numbers3[10];
+    for (int i = 0; i < 10; ++i) {
+        numbers3[i] = numbers[i];//NOWARN
+    }
+
+    return numbers3;
+}
+
+int* getNumbers4() {
+    int* numbers = getNumbers3();
+    static int numbers4[10];
+    for (int i = 0; i < 10; ++i) {
+        numbers4[i] = numbers[i];//WARN
+    }
+    return numbers4;
+}
+
+int main (void) {
+
+    int *numbers = getNumbers4();
+
+    for (int i = 0; i < 10; i++ ) {
+       printf( "%d\n", *(numbers + i));//NOWARN
+    }
+
+    return 0;
+}

From 6745d799de882a056df9dd0c695668592a5f31eb Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 22:49:37 +0200
Subject: [PATCH 058/104] Slightly refactor `check_count` and check for `src`'s
 size in `memcpy`

---
 src/analyses/memOutOfBounds.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 655ed7d3f1..8a2ca12467 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -372,22 +372,22 @@ struct
     | _ -> ()
 
   (* For memset() and memcpy() *)
-  let check_count ctx fun_name dest n =
+  let check_count ctx fun_name ptr n =
     let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in
     let cwe_number = 823 in
-    let dest_size = get_size_of_ptr_target ctx dest in
+    let ptr_size = get_size_of_ptr_target ctx ptr in
     let eval_n = ctx.ask (Queries.EvalInt n) in
-    let addr_offs = get_addr_offs ctx dest in
-    match dest_size, eval_n with
+    let addr_offs = get_addr_offs ctx ptr in
+    match ptr_size, eval_n with
     | `Top, _ ->
       set_mem_safety_flag InvalidDeref;
-      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name
+      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name
     | _, `Top ->
       set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name
     | `Bot, _ ->
       set_mem_safety_flag InvalidDeref;
-      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name
+      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name
     | _, `Bot ->
       set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name
@@ -399,7 +399,7 @@ struct
       begin match ID.to_bool dest_size_lt_count with
         | Some true ->
           set_mem_safety_flag InvalidDeref;
-          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en
         | Some false -> ()
         | None ->
           set_mem_safety_flag InvalidDeref;
@@ -436,7 +436,9 @@ struct
     (* Check calls to memset and memcpy for out-of-bounds-accesses *)
     match desc.special arglist with
     | Memset { dest; ch; count; } -> check_count ctx f.vname dest count;
-    | Memcpy { dest; src; n = count; } -> check_count ctx f.vname dest count;
+    | Memcpy { dest; src; n = count; } ->
+      check_count ctx f.vname src count;
+      check_count ctx f.vname dest count;
     | _ -> ();
     ctx.local
 

From 136bec0232107c61a42a3ed369a03aee90fbf2b8 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 22:50:41 +0200
Subject: [PATCH 059/104] Add test case with wrong src size for memcpy

---
 .../regression/77-mem-oob/12-memcpy-oob-src.c | 43 +++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 tests/regression/77-mem-oob/12-memcpy-oob-src.c

diff --git a/tests/regression/77-mem-oob/12-memcpy-oob-src.c b/tests/regression/77-mem-oob/12-memcpy-oob-src.c
new file mode 100644
index 0000000000..0f3a609fbe
--- /dev/null
+++ b/tests/regression/77-mem-oob/12-memcpy-oob-src.c
@@ -0,0 +1,43 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
+// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed
+#include <stdlib.h>
+#include <string.h>
+
+struct A {
+	unsigned char a;
+	unsigned char b:2;
+	unsigned char c:2;
+	unsigned char d:5;
+	unsigned char e;
+} __attribute__((packed));
+
+struct A d;
+int main(void)
+{
+	struct A *p;
+	p = malloc(5);
+	d.a = 1;
+	d.b = 2;
+	d.c = 3;
+	d.d = 4;
+	d.e = 5;
+    // It's an OOB error, because sizeof(d) == 4
+	memcpy(p, &d, 5); //WARN
+	if (p->a != 1) {
+		free(p);
+	}
+	if (p->b != 2) {
+		free(p);
+	}
+	if (p->c != 3) {
+		free(p);
+	}
+	if (p->d != 4) {
+		free(p);
+	}
+	if (p->e != 5) {
+		free(p);
+	}
+	free(p);
+}
+

From 3a2fe3f09278fc80fe8e6b68c3697f6996bf7030 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 4 Oct 2023 22:53:50 +0200
Subject: [PATCH 060/104] Correct test 77/07 to warn for src OOB access in
 memcpy as well

---
 tests/regression/77-mem-oob/07-memcpy-oob.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/77-mem-oob/07-memcpy-oob.c b/tests/regression/77-mem-oob/07-memcpy-oob.c
index 012f92996e..5605404a87 100644
--- a/tests/regression/77-mem-oob/07-memcpy-oob.c
+++ b/tests/regression/77-mem-oob/07-memcpy-oob.c
@@ -31,13 +31,13 @@ int main(int argc, char const *argv[]) {
     memcpy(a, b, 40); //WARN
     memcpy(a, b, sizeof(a)); //WARN
 
-    memcpy(b, a, 60); //NOWARN
+    memcpy(b, a, 60); //WARN
     b += 1;
     memcpy(b, a, 60); //WARN
 
 
     s *s_ptr = malloc(sizeof(s));
-    memcpy(s_ptr, a, sizeof(s)); //NOWARN
+    memcpy(s_ptr, a, sizeof(s)); //WARN
     memcpy(s_ptr->a, 0, sizeof(s)); //WARN
     memcpy(s_ptr->b, 0, sizeof(s)); //WARN
 

From 9b728d352169f0eea1e4a21609233413f2ae1c79 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 5 Oct 2023 13:59:19 +0200
Subject: [PATCH 061/104] Set `dest` in `memcpy` to top if `n` doesn't match
 its size

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a5b60e8cca..2d779b8d85 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2054,6 +2054,64 @@ struct
       AnalysisStateUtil.set_mem_safety_flag InvalidFree;
       M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname
 
+  let points_to_heap_only ctx ptr =
+    match ctx.ask (Queries.MayPointTo ptr) with
+    | a when not (Queries.AD.is_top a)->
+      Queries.AD.for_all (function
+          | Addr (v, o) -> ctx.ask (Queries.IsHeapVar v)
+          | _ -> false
+        ) a
+    | _ -> false
+
+  let get_size_of_ptr_target ctx ptr =
+    let intdom_of_int x =
+      ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
+    in
+    let size_of_type_in_bytes typ =
+      let typ_size_in_bytes = (bitsSizeOf typ) / 8 in
+      intdom_of_int typ_size_in_bytes
+    in
+    if points_to_heap_only ctx ptr then
+      (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
+      ctx.ask (Queries.BlobSize {exp = ptr; base_address = true})
+    else
+      match ctx.ask (Queries.MayPointTo ptr) with
+      | a when not (Queries.AD.is_top a) ->
+        let pts_list = Queries.AD.elements a in
+        let pts_elems_to_sizes (addr: Queries.AD.elt) =
+          begin match addr with
+            | Addr (v, _) ->
+              begin match v.vtype with
+                | TArray (item_typ, _, _) ->
+                  let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
+                  begin match ctx.ask (Queries.EvalLength ptr) with
+                    | `Lifted arr_len ->
+                      let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in
+                      begin
+                        try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
+                        with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
+                      end
+                    | `Bot -> `Bot
+                    | `Top -> `Top
+                  end
+                | _ ->
+                  let type_size_in_bytes = size_of_type_in_bytes v.vtype in
+                  `Lifted type_size_in_bytes
+              end
+            | _ -> `Top
+          end
+        in
+        (* Map each points-to-set element to its size *)
+        let pts_sizes = List.map pts_elems_to_sizes pts_list in
+        (* Take the smallest of all sizes that ptr's contents may have *)
+        begin match pts_sizes with
+          | [] -> `Bot
+          | [x] -> x
+          | x::xs -> List.fold_left ValueDomainQueries.ID.join x xs
+        end
+      | _ ->
+        (M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
+         `Top)
 
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
     let invalidate_ret_lv st = match lv with
@@ -2073,13 +2131,32 @@ struct
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in
-    let memory_copying dst src =
+    let memory_copying dst src n =
+      let dest_size = get_size_of_ptr_target ctx dst in
+      let n_intdom = match n with
+        | Some exp -> ctx.ask (Queries.EvalInt exp)
+        | None -> `Bot
+      in
+      let dest_size_equal_n =
+        match dest_size, n_intdom with
+        | `Top, `Top -> true
+        | `Bot, `Bot -> true
+        | `Lifted ds, `Lifted n ->
+          let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
+          let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
+          let ds_eq_n = ID.eq casted_ds casted_n in
+          begin match ID.to_bool ds_eq_n with
+            | Some b -> b
+            | None -> false
+          end
+        | _, _ -> false
+      in
       let dest_a, dest_typ = addr_type_of_exp dst in
       let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in
       let src_typ = eval_lv (Analyses.ask_of_ctx ctx) gs st src_lval
                     |> AD.type_of in
       (* when src and destination type coincide, take value from the source, otherwise use top *)
-      let value = if typeSig dest_typ = typeSig src_typ then
+      let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
           let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
           eval_rv (Analyses.ask_of_ctx ctx) gs st (Lval src_cast_lval)
         else
@@ -2140,13 +2217,13 @@ struct
       let value = VD.zero_init_value dest_typ in
       set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
     | Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *)
-      memory_copying dst src
+      memory_copying dst src (Some n)
     (* strcpy(dest, src); *)
     | Strcpy { dest = dst; src; n = None }, _ ->
       let dest_a, dest_typ = addr_type_of_exp dst in
       (* when dest surely isn't a string literal, try copying src to dest *)
       if AD.string_writing_defined dest_a then
-        memory_copying dst src
+        memory_copying dst src None
       else
         (* else return top (after a warning was issued) *)
         set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (VD.top_value (unrollType dest_typ))

From 48f2cfedda0a61517a69e012dfc07a08fe3646cb Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 5 Oct 2023 14:00:18 +0200
Subject: [PATCH 062/104] Add test case for UAF due to bad memcpy

---
 .../74-use_after_free/16-uaf-packed-struct.c  | 40 +++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 tests/regression/74-use_after_free/16-uaf-packed-struct.c

diff --git a/tests/regression/74-use_after_free/16-uaf-packed-struct.c b/tests/regression/74-use_after_free/16-uaf-packed-struct.c
new file mode 100644
index 0000000000..e10aa28486
--- /dev/null
+++ b/tests/regression/74-use_after_free/16-uaf-packed-struct.c
@@ -0,0 +1,40 @@
+// PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+#include <string.h>
+
+struct A {
+	unsigned char a;
+	unsigned char b:2;
+	unsigned char c:2;
+	unsigned char pad1[2];
+	unsigned int d;
+	unsigned char e;
+	unsigned char pad2[3];
+} __attribute__((packed));
+
+struct A d;
+int main(void)
+{
+	struct A *p;
+	p = malloc(12);
+	d.a = 1;
+	d.b = 2;
+	d.c = 3;
+	d.d = 4;
+	d.e = 5;
+	memcpy(p, &d, 4);
+	if (p->a != 1) {
+		free(p);
+	}
+	if (p->b != 2) {//WARN
+		free(p);//WARN
+	}
+	if (p->c != 3) {//WARN
+		free(p);//WARN
+	}
+	if (p->d != 4) { //WARN
+		free(p);//WARN
+	}
+	free(p);//WARN
+}
+

From 753b5c1661009bbfa6542fd64ca3d6de62231a34 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 5 Oct 2023 14:02:33 +0200
Subject: [PATCH 063/104] Check offsets of dereferenced lvalues as well

---
 src/analyses/memOutOfBounds.ml | 65 +++++++++++++++++++++++++++++++---
 1 file changed, 61 insertions(+), 4 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 8a2ca12467..d555db968d 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -122,9 +122,9 @@ struct
           | x::xs -> List.fold_left VDQ.ID.join x xs
         end
       | _ ->
-        set_mem_safety_flag InvalidDeref;
-        M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
-        `Top
+        (set_mem_safety_flag InvalidDeref;
+         M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
+         `Top)
 
   let get_ptr_deref_type ptr_typ =
     match ptr_typ with
@@ -165,6 +165,32 @@ struct
         with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
       end
 
+  let rec cil_offs_to_idx ctx typ offs =
+    match offs with
+    | NoOffset -> intdom_of_int 0
+    | Field (field, o) ->
+      let field_as_offset = Field (field, NoOffset) in
+      let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in
+      let bytes_offset = intdom_of_int (bits_offset / 8) in
+      let remaining_offset = cil_offs_to_idx ctx field.ftype o in
+      begin
+        try ID.add bytes_offset remaining_offset
+        with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+      end
+    | Index (x, o) ->
+      begin try
+          begin match ctx.ask (Queries.EvalInt x) with
+            | `Top -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
+            | `Bot -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+            | `Lifted eval_x ->
+              let typ_size_in_bytes = size_of_type_in_bytes typ in
+              let bytes_offset = ID.mul typ_size_in_bytes eval_x in
+              let remaining_offset = cil_offs_to_idx ctx typ o in
+              ID.add bytes_offset remaining_offset
+          end
+        with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+      end
+
   let check_unknown_addr_deref ctx ptr =
     let may_contain_unknown_addr =
       match ctx.ask (Queries.EvalValue ptr) with
@@ -245,7 +271,38 @@ struct
       match lval, is_implicitly_derefed with
       | (Var _, _), false -> ()
       | (Var v, _), true -> check_no_binop_deref ctx (Lval lval)
-      | (Mem e, _), _ ->
+      | (Mem e, o), _ ->
+        let ptr_deref_type = get_ptr_deref_type @@ typeOf e in
+        let offs_intdom = begin match ptr_deref_type with
+          | Some t -> cil_offs_to_idx ctx t o
+          | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+        end in
+        let e_size = get_size_of_ptr_target ctx e in
+        let () = begin match e_size with
+          | `Top ->
+            (set_mem_safety_flag InvalidDeref;
+             M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e)
+          | `Bot ->
+            (set_mem_safety_flag InvalidDeref;
+             M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e)
+          | `Lifted es ->
+            let casted_es = ID.cast_to (Cilfacade.ptrdiff_ikind ()) es in
+            let one = intdom_of_int 1 in
+            let casted_es = ID.sub casted_es one in
+            let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in
+            let ptr_size_lt_offs = ID.lt casted_es casted_offs in
+            let behavior = Undefined MemoryOutOfBoundsAccess in
+            let cwe_number = 823 in
+            begin match ID.to_bool ptr_size_lt_offs with
+              | Some true ->
+                (set_mem_safety_flag InvalidDeref;
+                 M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs)
+              | Some false -> ()
+              | None ->
+                (set_mem_safety_flag InvalidDeref;
+                 M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs)
+            end
+        end in
         begin match e with
           | Lval (Var v, _) as lval_exp -> check_no_binop_deref ctx lval_exp
           | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI ->

From d68328163e07f228f44f50c0b9b27200ea631284 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 5 Oct 2023 14:02:51 +0200
Subject: [PATCH 064/104] Add regr. test case for OOB due to too large lval
 offset

---
 .../77-mem-oob/13-mem-oob-packed-struct.c     | 33 +++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 tests/regression/77-mem-oob/13-mem-oob-packed-struct.c

diff --git a/tests/regression/77-mem-oob/13-mem-oob-packed-struct.c b/tests/regression/77-mem-oob/13-mem-oob-packed-struct.c
new file mode 100644
index 0000000000..552cd1bb0b
--- /dev/null
+++ b/tests/regression/77-mem-oob/13-mem-oob-packed-struct.c
@@ -0,0 +1,33 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+
+struct A {
+	unsigned char a;
+	unsigned char b:2;
+	unsigned char c:2;
+	unsigned char d;
+} __attribute__((packed));
+
+int main(void)
+{
+	struct A *p;
+	p = malloc(2);
+	p->a = 1;
+	if (p->a != 1) {
+		free(p);
+	}
+	p->b = 2;
+	if (p->b != 2) {
+		free(p);
+	}
+	p->c = 3;
+	if (p->c != 3) {
+		free(p);
+	}
+	p->d = 4; //WARN
+	if (p->d != 4) {//WARN
+		free(p);
+	}
+	free(p);
+}
+

From 22e4df53b11aa16dc676a690f131321f2112523b Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Thu, 5 Oct 2023 15:24:47 +0200
Subject: [PATCH 065/104] Fix exceptions due to ID ops

---
 src/analyses/base.ml           | 6 +++++-
 src/analyses/memOutOfBounds.ml | 9 +++++++--
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2d779b8d85..b6cc5c29cf 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2144,7 +2144,11 @@ struct
         | `Lifted ds, `Lifted n ->
           let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
           let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
-          let ds_eq_n = ID.eq casted_ds casted_n in
+          let ds_eq_n =
+            begin try ID.eq casted_ds casted_n
+              with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+            end
+          in
           begin match ID.to_bool ds_eq_n with
             | Some b -> b
             | None -> false
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index d555db968d..68dae1d89a 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -184,7 +184,8 @@ struct
             | `Bot -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
             | `Lifted eval_x ->
               let typ_size_in_bytes = size_of_type_in_bytes typ in
-              let bytes_offset = ID.mul typ_size_in_bytes eval_x in
+              let casted_eval_x = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eval_x in
+              let bytes_offset = ID.mul typ_size_in_bytes casted_eval_x in
               let remaining_offset = cil_offs_to_idx ctx typ o in
               ID.add bytes_offset remaining_offset
           end
@@ -290,7 +291,11 @@ struct
             let one = intdom_of_int 1 in
             let casted_es = ID.sub casted_es one in
             let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in
-            let ptr_size_lt_offs = ID.lt casted_es casted_offs in
+            let ptr_size_lt_offs =
+              begin try ID.lt casted_es casted_offs
+                with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+              end
+            in
             let behavior = Undefined MemoryOutOfBoundsAccess in
             let cwe_number = 823 in
             begin match ID.to_bool ptr_size_lt_offs with

From b9c213441f2ef03ce02173fa323650ebe234c080 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:54:55 +0300
Subject: [PATCH 066/104] Fix size check in `memory_copying`

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index b6cc5c29cf..6aaf25944e 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2139,21 +2139,16 @@ struct
       in
       let dest_size_equal_n =
         match dest_size, n_intdom with
-        | `Top, `Top -> true
-        | `Bot, `Bot -> true
         | `Lifted ds, `Lifted n ->
           let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
           let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
           let ds_eq_n =
             begin try ID.eq casted_ds casted_n
-              with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+              with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
             end
           in
-          begin match ID.to_bool ds_eq_n with
-            | Some b -> b
-            | None -> false
-          end
-        | _, _ -> false
+          Option.value ~default:false ID.to_bool ds_eq_n
+        | _ -> false
       in
       let dest_a, dest_typ = addr_type_of_exp dst in
       let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in

From 625e90b308159da7407f0fef01cd863bfc662d36 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:56:11 +0300
Subject: [PATCH 067/104] Use `Option.map_default` instead of `match`

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 src/analyses/base.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 6aaf25944e..cc5ddc9c9d 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2133,10 +2133,7 @@ struct
     let desc = LF.find f in
     let memory_copying dst src n =
       let dest_size = get_size_of_ptr_target ctx dst in
-      let n_intdom = match n with
-        | Some exp -> ctx.ask (Queries.EvalInt exp)
-        | None -> `Bot
-      in
+      let n_intdom = Option.map_default (fun exp -> ctx.ask (Queries.EvalInt exp)) `Bot n in
       let dest_size_equal_n =
         match dest_size, n_intdom with
         | `Lifted ds, `Lifted n ->

From fbab25ec49ecee2727f9675e36e5b3116b4c1d91 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:56:59 +0300
Subject: [PATCH 068/104] Use `_` in place of unused offset in lambda

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 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 cc5ddc9c9d..df67d1afe4 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2058,7 +2058,7 @@ struct
     match ctx.ask (Queries.MayPointTo ptr) with
     | a when not (Queries.AD.is_top a)->
       Queries.AD.for_all (function
-          | Addr (v, o) -> ctx.ask (Queries.IsHeapVar v)
+          | Addr (v, _) -> ctx.ask (Queries.IsHeapVar v)
           | _ -> false
         ) a
     | _ -> false

From 91aeee732f1f97afdb406e189176f22c46049ff1 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:57:46 +0300
Subject: [PATCH 069/104] Set `Cabs2cil.addNestedScopeAttr` based on the
 Goblint config option

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 src/util/cilfacade.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 432b623464..3b00365abf 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -41,8 +41,7 @@ let init_options () =
   Mergecil.merge_inlines := get_bool "cil.merge.inlines";
   Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
   Cil.gnu89inline := get_bool "cil.gnu89inline";
-  if get_bool "cil.addNestedScopeAttr" then
-    Cabs2cil.addNestedScopeAttr := true
+  Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";
 
 let init () =
   initCIL ();

From 992e5c0b183326d8a3acc102fd40c99e110c140d Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:04:44 +0200
Subject: [PATCH 070/104] Remove extra semicolon

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

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 3b00365abf..ba57074e5a 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -41,7 +41,7 @@ let init_options () =
   Mergecil.merge_inlines := get_bool "cil.merge.inlines";
   Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
   Cil.gnu89inline := get_bool "cil.gnu89inline";
-  Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";
+  Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr"
 
 let init () =
   initCIL ();

From cc351e04e745b11aaab409a60b7d2dc7a7c32eab Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:05:00 +0200
Subject: [PATCH 071/104] Use `Option.default` in place of `Option.value`

---
 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 df67d1afe4..f5da725226 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2144,7 +2144,7 @@ struct
               with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
             end
           in
-          Option.value ~default:false ID.to_bool ds_eq_n
+          Option.default false (ID.to_bool ds_eq_n)
         | _ -> false
       in
       let dest_a, dest_typ = addr_type_of_exp dst in

From de0220baf762f69ba6f0da19299ce568b243bed4 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Fri, 6 Oct 2023 23:09:46 +0200
Subject: [PATCH 072/104] Use `AD.exists` to warn about non-local vars in
 address set instead of using `AD.iter`

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index f5da725226..908dc88401 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1052,17 +1052,14 @@ struct
               AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
               M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer"
             );
-            (* Warn if any of the addresses contains a non-local variable *)
-            AD.iter (function
-                | AD.Addr.Addr (v,o) ->
-                  if not (CPA.mem v st.cpa) && not (is_global a v) then (
-                    (* TODO: Not the smartest move to set the global flag within an iter *)
-                    (* TODO: We can resort to using AD.exists instead *)
-                    AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
-                    M.warn "lval %a points to non-local variable %a. Invalid pointer dereference may occur" d_lval lval CilType.Varinfo.pretty v
-                  )
-                | _ -> ()
-              ) adr
+            (* Warn if any of the addresses contains a non-local and non-global variable *)
+            if AD.exists (function
+                | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v)
+                | _ -> false
+              ) adr then (
+              AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
+              M.warn "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval
+            )
           );
           AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
         | _ ->

From fd5237a6dfdd68f1cd6791030dd43227e9ed77fc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 11:40:54 +0300
Subject: [PATCH 073/104] Add 68-longjmp/56-longjmp-top extracted from concrat

---
 tests/regression/68-longjmp/56-longjmp-top.c | 21 ++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 tests/regression/68-longjmp/56-longjmp-top.c

diff --git a/tests/regression/68-longjmp/56-longjmp-top.c b/tests/regression/68-longjmp/56-longjmp-top.c
new file mode 100644
index 0000000000..4a12a43792
--- /dev/null
+++ b/tests/regression/68-longjmp/56-longjmp-top.c
@@ -0,0 +1,21 @@
+// Extracted from concrat/pigz.
+#include <setjmp.h>
+#include <pthread.h>
+#include <goblint.h>
+
+pthread_key_t buf_key;
+
+int main() {
+  jmp_buf buf;
+  pthread_setspecific(buf_key, &buf);
+
+  if (!setjmp(buf)) {
+    jmp_buf *buf_ptr;
+    buf_ptr = pthread_getspecific(buf_key);
+    longjmp(*buf_ptr, 1); // TODO NO CRASH: problem?!
+  }
+  else {
+    __goblint_check(1); // reachable
+  }
+  return 0;
+}

From 2224e86ce5e770cedd4558cfff6379471424e743 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 11:46:24 +0300
Subject: [PATCH 074/104] Fix longjmp crash on Uninitialized

---
 src/analyses/base.ml                         | 11 +++++++++--
 tests/regression/68-longjmp/56-longjmp-top.c |  2 +-
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 7b87d3ff51..2fda2540e8 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1217,9 +1217,16 @@ struct
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
               x
-            | y -> failwith (GobPretty.sprintf "problem?! is %a %a:\n state is %a" CilType.Exp.pretty e VD.pretty y D.pretty ctx.local)
+            | Top
+            | Bot ->
+              JmpBufDomain.JmpBufSet.top ()
+            | y ->
+              M.debug ~category:Imprecise "EvalJmpBuf %a is %a, not JmpBuf." CilType.Exp.pretty e VD.pretty y;
+              JmpBufDomain.JmpBufSet.top ()
           end
-        | _ -> failwith "problem?!"
+        | _ ->
+          M.debug ~category:Imprecise "EvalJmpBuf is not Address";
+          JmpBufDomain.JmpBufSet.top ()
       end
     | Q.EvalInt e ->
       query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
diff --git a/tests/regression/68-longjmp/56-longjmp-top.c b/tests/regression/68-longjmp/56-longjmp-top.c
index 4a12a43792..4d57b42fd3 100644
--- a/tests/regression/68-longjmp/56-longjmp-top.c
+++ b/tests/regression/68-longjmp/56-longjmp-top.c
@@ -12,7 +12,7 @@ int main() {
   if (!setjmp(buf)) {
     jmp_buf *buf_ptr;
     buf_ptr = pthread_getspecific(buf_key);
-    longjmp(*buf_ptr, 1); // TODO NO CRASH: problem?!
+    longjmp(*buf_ptr, 1); // NO CRASH: problem?!
   }
   else {
     __goblint_check(1); // reachable

From 56cf37e347039f9a2f12cfd360f0dece5e583c5a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 12:50:22 +0300
Subject: [PATCH 075/104] Add missing library functions for concrat/dnspod-sr

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 1c509e7660..8566cd6b0c 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -265,6 +265,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("access", unknown [drop "pathname" [r]; drop "mode" []]);
     ("ttyname", unknown ~attrs:[ThreadUnsafe] [drop "fd" []]);
     ("shm_open", unknown [drop "name" [r]; drop "oflag" []; drop "mode" []]);
+    ("shmget", unknown [drop "key" []; drop "size" []; drop "shmflag" []]);
+    ("shmat", unknown [drop "shmid" []; drop "shmaddr" []; drop "shmflag" []]) (* TODO: shmaddr? *);
+    ("shmdt", unknown [drop "shmaddr" []]) (* TODO: shmaddr? *);
     ("sched_get_priority_max", unknown [drop "policy" []]);
     ("mprotect", unknown [drop "addr" []; drop "len" []; drop "prot" []]);
     ("ftime", unknown [drop "tp" [w]]);
@@ -364,6 +367,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("sigdelset", unknown [drop "set" [r; w]; drop "signum" []]);
     ("sigismember", unknown [drop "set" [r]; drop "signum" []]);
     ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]);
+    ("sigwait", unknown [drop "set" [r]; drop "sig" [w]]);
+    ("sigwaitinfo", unknown [drop "set" [r]; drop "info" [w]]);
+    ("sigtimedwait", unknown [drop "set" [r]; drop "info" [w]; drop "timeout" [r]]);
     ("fork", unknown []);
     ("dlopen", unknown [drop "filename" [r]; drop "flag" []]);
     ("dlerror", unknown ~attrs:[ThreadUnsafe] []);
@@ -566,6 +572,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("atoq", unknown [drop "nptr" [r]]);
     ("strchrnul", unknown [drop "s" [r]; drop "c" []]);
     ("getdtablesize", unknown []);
+    ("daemon", unknown [drop "nochdir" []; drop "noclose" []]);
   ]
 
 let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -1135,7 +1142,6 @@ let invalidate_actions = [
     "umount", readsAll;(*safe*)
     "scandir", writes [1;3;4];(*keep [1;3;4]*)
     "unlink", readsAll;(*safe*)
-    "sigwait", writesAllButFirst 1 readsAll;(*drop 1*)
     "bindtextdomain", readsAll;(*safe*)
     "textdomain", readsAll;(*safe*)
     "dcgettext", readsAll;(*safe*)

From a13e2b921268d7b4f894494a32424ed952c4b145 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 12:54:12 +0300
Subject: [PATCH 076/104] Add mremap library function for concrat/kona

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 8566cd6b0c..87534e97bb 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -589,6 +589,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__xpg_basename", unknown [drop "path" [r]]);
     ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *)
     ("madvise", unknown [drop "addr" []; drop "length" []; drop "advice" []]);
+    ("mremap", unknown (drop "old_address" [] :: drop "old_size" [] :: drop "new_size" [] :: drop "flags" [] :: VarArgs (drop "new_address" [])));
     ("inotify_init1", unknown [drop "flags" []]);
     ("inotify_add_watch", unknown [drop "fd" []; drop "pathname" [r]; drop "mask" []]);
     ("inotify_rm_watch", unknown [drop "fd" []; drop "wd" []]);

From 530781376bfc10281fd0a3451e7bb683d3e28141 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:03:11 +0300
Subject: [PATCH 077/104] Add missing library functions for concrat/lmdb

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 87534e97bb..a1a79f5f5c 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -246,6 +246,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("mkfifo", unknown [drop "pathname" [r]; drop "mode" []]);
     ("ntohs", unknown [drop "netshort" []]);
     ("alarm", unknown [drop "seconds" []]);
+    ("pread", unknown [drop "fd" []; drop "buf" [w]; drop "count" []; drop "offset" []]);
     ("pwrite", unknown [drop "fd" []; drop "buf" [r]; drop "count" []; drop "offset" []]);
     ("hstrerror", unknown [drop "err" []]);
     ("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]);
@@ -379,6 +380,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("uname", unknown [drop "buf" [w_deep]]);
     ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]);
     ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]);
+    ("fsync", unknown [drop "fd" []]);
+    ("fdatasync", unknown [drop "fd" []]);
   ]
 
 (** Pthread functions. *)
@@ -443,6 +446,10 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_attr_setschedpolicy", unknown [drop "attr" [r; w]; drop "policy" []]);
     ("pthread_condattr_init", unknown [drop "attr" [w]]);
     ("pthread_condattr_setclock", unknown [drop "attr" [w]; drop "clock_id" []]);
+    ("pthread_mutexattr_getpshared", unknown [drop "attr" [r]; drop "pshared" [w]]);
+    ("pthread_mutexattr_setpshared", unknown [drop "attr" [w]; drop "pshared" []]);
+    ("pthread_mutexattr_getrobust", unknown [drop "attr" [r]; drop "pshared" [w]]);
+    ("pthread_mutexattr_setrobust", unknown [drop "attr" [w]; drop "pshared" []]);
     ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
     ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
     ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
@@ -590,12 +597,15 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *)
     ("madvise", unknown [drop "addr" []; drop "length" []; drop "advice" []]);
     ("mremap", unknown (drop "old_address" [] :: drop "old_size" [] :: drop "new_size" [] :: drop "flags" [] :: VarArgs (drop "new_address" [])));
+    ("msync", unknown [drop "addr" []; drop "len" []; drop "flags" []]);
     ("inotify_init1", unknown [drop "flags" []]);
     ("inotify_add_watch", unknown [drop "fd" []; drop "pathname" [r]; drop "mask" []]);
     ("inotify_rm_watch", unknown [drop "fd" []; drop "wd" []]);
     ("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *)
     ("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]);
     ("fts_close", unknown [drop "ftsp" [f_deep]]);
+    ("statfs", unknown [drop "path" [r]; drop "buf" [w]]);
+    ("fstatfs", unknown [drop "fd" []; drop "buf" [w]]);
   ]
 
 let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
@@ -1134,7 +1144,6 @@ let invalidate_actions = [
     "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
     "umount2", readsAll;(*safe*)
     "waitpid", readsAll;(*safe*)
-    "statfs", writes [1;3;4];(*keep [1;3;4]*)
     "mount", readsAll;(*safe*)
     "__open_alias", readsAll;(*safe*)
     "__open_2", readsAll;(*safe*)

From 25ef4ce6f33be1406b9af3e0c8ca1ed3a20e0474 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:12:07 +0300
Subject: [PATCH 078/104] Add missing library functions for concrat/minimap2

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index a1a79f5f5c..af96e10c06 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -42,6 +42,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("getc", unknown [drop "stream" [r_deep; w_deep]]);
     ("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]);
+    ("freopen", unknown [drop "pathname" [r]; drop "mode" [r]; drop "stream" [r_deep; w_deep]]);
     ("printf", unknown (drop "format" [r] :: VarArgs (drop' [r])));
     ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' [r])));
     ("sprintf", unknown (drop "buffer" [w] :: drop "format" [r] :: VarArgs (drop' [r])));
@@ -382,6 +383,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]);
     ("fsync", unknown [drop "fd" []]);
     ("fdatasync", unknown [drop "fd" []]);
+    ("getrusage", unknown [drop "who" []; drop "usage" [w]]);
   ]
 
 (** Pthread functions. *)
@@ -987,6 +989,10 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]);
     ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]);
     ("inflateEnd", unknown [drop "strm" [f_deep]]);
+    ("gzopen", unknown [drop "path" [r]; drop "mode" [r]]);
+    ("gzdopen", unknown [drop "fd" []; drop "mode" [r]]);
+    ("gzread", unknown [drop "file" [r_deep; w_deep]; drop "buf" [w]; drop "len" []]);
+    ("gzclose", unknown [drop "file" [f_deep]]);
   ]
 
 let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[

From 9f614ebbd474a0c8b9696a39cbd63620e24e3ae4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:21:03 +0300
Subject: [PATCH 079/104] Add missing library functions for concrat/phpspy

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index af96e10c06..c795c04084 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -111,6 +111,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("asprintf", unknown (drop "strp" [w] :: drop "format" [r] :: VarArgs (drop' [r_deep]))); (* TODO: glibc section? *)
     ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("mktime", unknown [drop "tm" [r;w]]);
@@ -339,6 +340,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r])));
     ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]);
     ("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]);
+    ("wcwidth", unknown [drop "c" []]);
     ("wcswidth", unknown [drop "s" [r]; drop "n" []]);
     ("link", unknown [drop "oldpath" [r]; drop "newpath" [r]]);
     ("renameat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]]);
@@ -518,6 +520,12 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__atomic_clear", unknown [drop "ptr" [w]; drop "memorder" []]);
     ("__atomic_compare_exchange_n", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" []; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]);
     ("__atomic_compare_exchange", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" [r]; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]);
+    ("__atomic_add_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_sub_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_and_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_xor_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_or_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_nand_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
     ("__atomic_fetch_add", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
     ("__atomic_fetch_sub", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
     ("__atomic_fetch_and", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
@@ -608,6 +616,8 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("fts_close", unknown [drop "ftsp" [f_deep]]);
     ("statfs", unknown [drop "path" [r]; drop "buf" [w]]);
     ("fstatfs", unknown [drop "fd" []; drop "buf" [w]]);
+    ("cfmakeraw", unknown [drop "termios" [r; w]]);
+    ("process_vm_readv", unknown [drop "pid" []; drop "local_iov" [w_deep]; drop "liovcnt" []; drop "remote_iov" []; drop "riovcnt" []; drop "flags" []]);
   ]
 
 let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))

From c22250889672d27f11aa99a33593218a70502bad Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:22:49 +0300
Subject: [PATCH 080/104] Add alphasort library function for
 concrat/ProcDump-for-Linux

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index c795c04084..2ea99cdcaa 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -386,6 +386,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("fsync", unknown [drop "fd" []]);
     ("fdatasync", unknown [drop "fd" []]);
     ("getrusage", unknown [drop "who" []; drop "usage" [w]]);
+    ("alphasort", unknown [drop "a" [r]; drop "b" [r]]);
   ]
 
 (** Pthread functions. *)

From 969d3156b879ba6a22f3d752945d320364e917e6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:43:02 +0300
Subject: [PATCH 081/104] Add missing library functions for concrat/Remotery

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 2ea99cdcaa..1247a66497 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -395,6 +395,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
     ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
     ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
+    ("pthread_equal", unknown [drop "t1" []; drop "t2" []]);
     ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
     ("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
     ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond);
@@ -535,6 +536,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__atomic_fetch_nand", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
     ("__atomic_test_and_set", unknown [drop "ptr" [r; w]; drop "memorder" []]);
     ("__atomic_thread_fence", unknown [drop "memorder" []]);
+    ("__sync_bool_compare_and_swap", unknown [drop "ptr" [r; w]; drop "oldval" []; drop "newval" []]);
     ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);

From 012282132c4fc362ee111e2fe91e90da4752610a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:56:58 +0300
Subject: [PATCH 082/104] Add missing library functions for concrat/siege

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 1247a66497..7bc373e3cc 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -387,6 +387,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("fdatasync", unknown [drop "fd" []]);
     ("getrusage", unknown [drop "who" []; drop "usage" [w]]);
     ("alphasort", unknown [drop "a" [r]; drop "b" [r]]);
+    ("gmtime_r", unknown [drop "timer" [r]; drop "result" [w]]);
+    ("rand_r", special [drop "seedp" [r; w]] Rand);
   ]
 
 (** Pthread functions. *)
@@ -447,6 +449,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]);
     ("pthread_key_delete", unknown [drop "key" [f]]);
     ("pthread_cancel", unknown [drop "thread" []]);
+    ("pthread_testcancel", unknown []);
+    ("pthread_setcancelstate", unknown [drop "state" []; drop "oldstate" [w]]);
     ("pthread_setcanceltype", unknown [drop "type" []; drop "oldtype" [w]]);
     ("pthread_detach", unknown [drop "thread" []]);
     ("pthread_attr_setschedpolicy", unknown [drop "attr" [r; w]; drop "policy" []]);

From c630a3926f71b740e002ae4ff6e6bdf515142cf4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 13:57:09 +0300
Subject: [PATCH 083/104] Add warn library function for
 concrat/the_silver_searcher

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 7bc373e3cc..62dbe2aa7c 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -551,7 +551,8 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("fputs_unlocked", unknown [drop "s" [r]; drop "stream" [w]]);
     ("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]);
-    ("error", unknown ((drop "status" []):: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
+    ("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
+    ("warn", unknown (drop "format" [r] :: VarArgs (drop' [r])));
     ("gettext", unknown [drop "msgid" [r]]);
     ("euidaccess", unknown [drop "pathname" [r]; drop "mode" []]);
     ("rpmatch", unknown [drop "response" [r]]);

From 0af8ba71bac405e1e7ade51607cee49f91dd2f3a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 14:39:47 +0300
Subject: [PATCH 084/104] Add zError library function for
 concrat/the_silver_searcher

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 62dbe2aa7c..03a984fede 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -1007,6 +1007,7 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]);
     ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]);
     ("inflateEnd", unknown [drop "strm" [f_deep]]);
+    ("zError", unknown [drop "err" []]);
     ("gzopen", unknown [drop "path" [r]; drop "mode" [r]]);
     ("gzdopen", unknown [drop "fd" []; drop "mode" [r]]);
     ("gzread", unknown [drop "file" [r_deep; w_deep]; drop "buf" [w]; drop "len" []]);

From 85ce4b252b47aebc19574938f0db01635c93114c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 10 Oct 2023 14:52:23 +0300
Subject: [PATCH 085/104] Add some missing library functions for
 concrat/sysbench

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

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 03a984fede..b84ddc5ac5 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -389,6 +389,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("alphasort", unknown [drop "a" [r]; drop "b" [r]]);
     ("gmtime_r", unknown [drop "timer" [r]; drop "result" [w]]);
     ("rand_r", special [drop "seedp" [r; w]] Rand);
+    ("srandom", unknown [drop "seed" []]);
+    ("random", special [] Rand);
+    ("posix_memalign", unknown [drop "memptr" [w]; drop "alignment" []; drop "size" []]); (* TODO: Malloc *)
   ]
 
 (** Pthread functions. *)

From e98911df182e6725bed56113613e30e7cd9f7fa1 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 11 Oct 2023 11:53:06 +0300
Subject: [PATCH 086/104] Remove unnecessary pin

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 goblint.opam.locked | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/goblint.opam.locked b/goblint.opam.locked
index d5af6ea348..2744d2fe92 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -122,9 +122,6 @@ build: [
 ]
 dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
-]
 conflicts: [
   "result" {< "1.5"}
 ]

From 072f99d701ddf09a97c9a7ab0b754be4c63ee138 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 11 Oct 2023 10:57:37 +0200
Subject: [PATCH 087/104] Remove commented out code from `enter` in UAF
 analysis

Add TODOs for future improvement there
---
 src/analyses/useAfterFree.ml | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 521f17d97f..ef63ab3e91 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -182,18 +182,10 @@ struct
   let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let caller_state = ctx.local in
     List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args;
+    (* TODO: The 2nd component of the callee state needs to contain only the heap vars from the caller state which are reachable from: *)
+    (* * Global program variables *)
+    (* * The callee arguments *)
     [caller_state, (AllocaVars.empty (), snd caller_state)]
-  (* if AllocaVars.is_empty (fst caller_state) && HeapVars.is_empty (snd caller_state) then
-      [caller_state, caller_state]
-    else (
-      let reachable_from_args = List.fold_left (fun ad arg -> Queries.AD.join ad (ctx.ask (ReachableFrom arg))) (Queries.AD.empty ()) args in
-      if Queries.AD.is_top reachable_from_args || D.is_top caller_state then
-        [caller_state, caller_state]
-      else
-        let reachable_vars = Queries.AD.to_var_may reachable_from_args in
-        let callee_state = (AllocaVars.empty (), HeapVars.filter (fun var -> List.mem var reachable_vars) (snd caller_state)) in (* TODO: use AD.mem directly *)
-        [caller_state, callee_state]
-        ) *)
 
   let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t =
     let (caller_stack_state, caller_heap_state) = ctx.local in

From e339ed17c88a154785a0d70ab4ad1c1c0aa31730 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 11 Oct 2023 11:59:50 +0300
Subject: [PATCH 088/104] Remove unnecessary stuff from test case `74/15`

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 tests/regression/74-use_after_free/15-juliet-uaf-global-var.c | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c b/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c
index 9cb3b2b29a..cc9819950f 100644
--- a/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c
+++ b/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c
@@ -1,7 +1,5 @@
-//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins
+//PARAM: --set ana.activated[+] useAfterFree
 #include <stdlib.h>
-#include <stdio.h>
-#include <pthread.h>
 
 int *global;
 

From f018ea37bc1e2cfb66237283b44a8400fc5cf161 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 11 Oct 2023 11:36:01 +0200
Subject: [PATCH 089/104] Reduce duplication

---
 src/analyses/memOutOfBounds.ml | 45 ++++++++++++++--------------------
 1 file changed, 18 insertions(+), 27 deletions(-)

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 68dae1d89a..d52bb1109a 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -165,32 +165,23 @@ struct
         with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
       end
 
-  let rec cil_offs_to_idx ctx typ offs =
-    match offs with
-    | NoOffset -> intdom_of_int 0
-    | Field (field, o) ->
-      let field_as_offset = Field (field, NoOffset) in
-      let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in
-      let bytes_offset = intdom_of_int (bits_offset / 8) in
-      let remaining_offset = cil_offs_to_idx ctx field.ftype o in
-      begin
-        try ID.add bytes_offset remaining_offset
-        with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
-      end
-    | Index (x, o) ->
-      begin try
-          begin match ctx.ask (Queries.EvalInt x) with
-            | `Top -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
-            | `Bot -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
-            | `Lifted eval_x ->
-              let typ_size_in_bytes = size_of_type_in_bytes typ in
-              let casted_eval_x = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eval_x in
-              let bytes_offset = ID.mul typ_size_in_bytes casted_eval_x in
-              let remaining_offset = cil_offs_to_idx ctx typ o in
-              ID.add bytes_offset remaining_offset
-          end
-        with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
-      end
+  let cil_offs_to_idx ctx typ offs =
+    (* TODO: Some duplication with convert_offset in base.ml, unclear how to immediately get more reuse *)
+    let rec convert_offset (ofs: offset) =
+      match ofs with
+      | NoOffset -> `NoOffset
+      | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
+      | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+        `Index (ID.top (), convert_offset ofs)
+      | Index (exp, ofs) ->
+        let i = match ctx.ask (Queries.EvalInt exp) with
+          | `Lifted x -> x
+          | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
+        in
+        `Index (i, convert_offset ofs)
+    in
+    PreValueDomain.Offs.to_index (convert_offset offs)
+
 
   let check_unknown_addr_deref ctx ptr =
     let may_contain_unknown_addr =
@@ -517,4 +508,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)

From a2f36fb4179705a812cc3b0f589d5fd0c9649dc9 Mon Sep 17 00:00:00 2001
From: Stanimir Bozhilov <stanimir.bozhilov.1998@gmail.com>
Date: Wed, 11 Oct 2023 16:46:33 +0200
Subject: [PATCH 090/104] Reorganize memsafety regr. tests

---
 .../{77-mem-oob => 74-invalid_deref}/01-oob-heap-simple.c         | 0
 .../{74-use_after_free => 74-invalid_deref}/02-conditional-uaf.c  | 0
 .../{74-use_after_free => 74-invalid_deref}/03-nested-ptr-uaf.c   | 0
 .../04-function-call-uaf.c                                        | 0
 .../{77-mem-oob => 74-invalid_deref}/05-oob-implicit-deref.c      | 0
 tests/regression/{77-mem-oob => 74-invalid_deref}/06-memset-oob.c | 0
 tests/regression/{77-mem-oob => 74-invalid_deref}/07-memcpy-oob.c | 0
 .../{77-mem-oob => 74-invalid_deref}/08-memset-memcpy-array.c     | 0
 .../{74-use_after_free => 74-invalid_deref}/09-juliet-uaf.c       | 0
 .../{77-mem-oob => 74-invalid_deref}/10-oob-two-loops.c           | 0
 .../{77-mem-oob => 74-invalid_deref}/11-address-offset-oob.c      | 0
 .../{77-mem-oob => 74-invalid_deref}/12-memcpy-oob-src.c          | 0
 .../{77-mem-oob => 74-invalid_deref}/13-mem-oob-packed-struct.c   | 0
 .../{74-use_after_free => 74-invalid_deref}/14-alloca-uaf.c       | 0
 .../15-juliet-uaf-global-var.c                                    | 0
 .../16-uaf-packed-struct.c                                        | 0
 .../17-scopes-no-static.c}                                        | 0
 .../01-simple-uaf.c => 74-invalid_deref/18-simple-uaf.c}          | 0
 .../19-oob-stack-simple.c}                                        | 0
 .../20-scopes-global-var.c}                                       | 0
 .../{77-mem-oob/03-oob-loop.c => 74-invalid_deref/21-oob-loop.c}  | 0
 .../03-scopes-static.c => 74-invalid_deref/22-scopes-static.c}    | 0
 .../23-oob-deref-after-ptr-arith.c}                               | 0
 .../24-uaf-free-in-wrapper-fun.c}                                 | 0
 .../06-uaf-struct.c => 74-invalid_deref/25-uaf-struct.c}          | 0
 .../26-memset-memcpy-addr-offs.c}                                 | 0
 .../27-wrapper-funs-uaf.c}                                        | 0
 .../28-multi-threaded-uaf.c}                                      | 0
 .../29-multi-threaded-uaf-with-joined-thread.c}                   | 0
 .../01-invalid-dealloc-simple.c                                   | 0
 .../02-invalid-dealloc-struct.c                                   | 0
 .../03-invalid-dealloc-array.c                                    | 0
 .../{75-invalid_dealloc => 75-invalid_free}/04-invalid-realloc.c  | 0
 .../{75-invalid_dealloc => 75-invalid_free}/05-free-at-offset.c   | 0
 .../06-realloc-at-offset.c                                        | 0
 .../07-free-at-struct-offset.c                                    | 0
 .../08-itc-no-double-free.c                                       | 0
 .../09-juliet-invalid-dealloc-alloca.c                            | 0
 .../10-invalid-dealloc-union.c                                    | 0
 .../07-itc-double-free.c => 75-invalid_free/11-itc-double-free.c} | 0
 .../12-realloc-at-struct-offset.c}                                | 0
 .../13-juliet-double-free.c}                                      | 0
 42 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/01-oob-heap-simple.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/02-conditional-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/03-nested-ptr-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/04-function-call-uaf.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/05-oob-implicit-deref.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/06-memset-oob.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/07-memcpy-oob.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/08-memset-memcpy-array.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/09-juliet-uaf.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/10-oob-two-loops.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/11-address-offset-oob.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/12-memcpy-oob-src.c (100%)
 rename tests/regression/{77-mem-oob => 74-invalid_deref}/13-mem-oob-packed-struct.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/14-alloca-uaf.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/15-juliet-uaf-global-var.c (100%)
 rename tests/regression/{74-use_after_free => 74-invalid_deref}/16-uaf-packed-struct.c (100%)
 rename tests/regression/{78-invalid-deref-scopes/01-scopes-no-static.c => 74-invalid_deref/17-scopes-no-static.c} (100%)
 rename tests/regression/{74-use_after_free/01-simple-uaf.c => 74-invalid_deref/18-simple-uaf.c} (100%)
 rename tests/regression/{77-mem-oob/02-oob-stack-simple.c => 74-invalid_deref/19-oob-stack-simple.c} (100%)
 rename tests/regression/{78-invalid-deref-scopes/02-scopes-global-var.c => 74-invalid_deref/20-scopes-global-var.c} (100%)
 rename tests/regression/{77-mem-oob/03-oob-loop.c => 74-invalid_deref/21-oob-loop.c} (100%)
 rename tests/regression/{78-invalid-deref-scopes/03-scopes-static.c => 74-invalid_deref/22-scopes-static.c} (100%)
 rename tests/regression/{77-mem-oob/04-oob-deref-after-ptr-arith.c => 74-invalid_deref/23-oob-deref-after-ptr-arith.c} (100%)
 rename tests/regression/{74-use_after_free/05-uaf-free-in-wrapper-fun.c => 74-invalid_deref/24-uaf-free-in-wrapper-fun.c} (100%)
 rename tests/regression/{74-use_after_free/06-uaf-struct.c => 74-invalid_deref/25-uaf-struct.c} (100%)
 rename tests/regression/{77-mem-oob/09-memset-memcpy-addr-offs.c => 74-invalid_deref/26-memset-memcpy-addr-offs.c} (100%)
 rename tests/regression/{74-use_after_free/11-wrapper-funs-uaf.c => 74-invalid_deref/27-wrapper-funs-uaf.c} (100%)
 rename tests/regression/{74-use_after_free/12-multi-threaded-uaf.c => 74-invalid_deref/28-multi-threaded-uaf.c} (100%)
 rename tests/regression/{74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c => 74-invalid_deref/29-multi-threaded-uaf-with-joined-thread.c} (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/01-invalid-dealloc-simple.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/02-invalid-dealloc-struct.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/03-invalid-dealloc-array.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/04-invalid-realloc.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/05-free-at-offset.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/06-realloc-at-offset.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/07-free-at-struct-offset.c (100%)
 rename tests/regression/{74-use_after_free => 75-invalid_free}/08-itc-no-double-free.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/09-juliet-invalid-dealloc-alloca.c (100%)
 rename tests/regression/{75-invalid_dealloc => 75-invalid_free}/10-invalid-dealloc-union.c (100%)
 rename tests/regression/{74-use_after_free/07-itc-double-free.c => 75-invalid_free/11-itc-double-free.c} (100%)
 rename tests/regression/{75-invalid_dealloc/08-realloc-at-struct-offset.c => 75-invalid_free/12-realloc-at-struct-offset.c} (100%)
 rename tests/regression/{74-use_after_free/10-juliet-double-free.c => 75-invalid_free/13-juliet-double-free.c} (100%)

diff --git a/tests/regression/77-mem-oob/01-oob-heap-simple.c b/tests/regression/74-invalid_deref/01-oob-heap-simple.c
similarity index 100%
rename from tests/regression/77-mem-oob/01-oob-heap-simple.c
rename to tests/regression/74-invalid_deref/01-oob-heap-simple.c
diff --git a/tests/regression/74-use_after_free/02-conditional-uaf.c b/tests/regression/74-invalid_deref/02-conditional-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/02-conditional-uaf.c
rename to tests/regression/74-invalid_deref/02-conditional-uaf.c
diff --git a/tests/regression/74-use_after_free/03-nested-ptr-uaf.c b/tests/regression/74-invalid_deref/03-nested-ptr-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/03-nested-ptr-uaf.c
rename to tests/regression/74-invalid_deref/03-nested-ptr-uaf.c
diff --git a/tests/regression/74-use_after_free/04-function-call-uaf.c b/tests/regression/74-invalid_deref/04-function-call-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/04-function-call-uaf.c
rename to tests/regression/74-invalid_deref/04-function-call-uaf.c
diff --git a/tests/regression/77-mem-oob/05-oob-implicit-deref.c b/tests/regression/74-invalid_deref/05-oob-implicit-deref.c
similarity index 100%
rename from tests/regression/77-mem-oob/05-oob-implicit-deref.c
rename to tests/regression/74-invalid_deref/05-oob-implicit-deref.c
diff --git a/tests/regression/77-mem-oob/06-memset-oob.c b/tests/regression/74-invalid_deref/06-memset-oob.c
similarity index 100%
rename from tests/regression/77-mem-oob/06-memset-oob.c
rename to tests/regression/74-invalid_deref/06-memset-oob.c
diff --git a/tests/regression/77-mem-oob/07-memcpy-oob.c b/tests/regression/74-invalid_deref/07-memcpy-oob.c
similarity index 100%
rename from tests/regression/77-mem-oob/07-memcpy-oob.c
rename to tests/regression/74-invalid_deref/07-memcpy-oob.c
diff --git a/tests/regression/77-mem-oob/08-memset-memcpy-array.c b/tests/regression/74-invalid_deref/08-memset-memcpy-array.c
similarity index 100%
rename from tests/regression/77-mem-oob/08-memset-memcpy-array.c
rename to tests/regression/74-invalid_deref/08-memset-memcpy-array.c
diff --git a/tests/regression/74-use_after_free/09-juliet-uaf.c b/tests/regression/74-invalid_deref/09-juliet-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/09-juliet-uaf.c
rename to tests/regression/74-invalid_deref/09-juliet-uaf.c
diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/74-invalid_deref/10-oob-two-loops.c
similarity index 100%
rename from tests/regression/77-mem-oob/10-oob-two-loops.c
rename to tests/regression/74-invalid_deref/10-oob-two-loops.c
diff --git a/tests/regression/77-mem-oob/11-address-offset-oob.c b/tests/regression/74-invalid_deref/11-address-offset-oob.c
similarity index 100%
rename from tests/regression/77-mem-oob/11-address-offset-oob.c
rename to tests/regression/74-invalid_deref/11-address-offset-oob.c
diff --git a/tests/regression/77-mem-oob/12-memcpy-oob-src.c b/tests/regression/74-invalid_deref/12-memcpy-oob-src.c
similarity index 100%
rename from tests/regression/77-mem-oob/12-memcpy-oob-src.c
rename to tests/regression/74-invalid_deref/12-memcpy-oob-src.c
diff --git a/tests/regression/77-mem-oob/13-mem-oob-packed-struct.c b/tests/regression/74-invalid_deref/13-mem-oob-packed-struct.c
similarity index 100%
rename from tests/regression/77-mem-oob/13-mem-oob-packed-struct.c
rename to tests/regression/74-invalid_deref/13-mem-oob-packed-struct.c
diff --git a/tests/regression/74-use_after_free/14-alloca-uaf.c b/tests/regression/74-invalid_deref/14-alloca-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/14-alloca-uaf.c
rename to tests/regression/74-invalid_deref/14-alloca-uaf.c
diff --git a/tests/regression/74-use_after_free/15-juliet-uaf-global-var.c b/tests/regression/74-invalid_deref/15-juliet-uaf-global-var.c
similarity index 100%
rename from tests/regression/74-use_after_free/15-juliet-uaf-global-var.c
rename to tests/regression/74-invalid_deref/15-juliet-uaf-global-var.c
diff --git a/tests/regression/74-use_after_free/16-uaf-packed-struct.c b/tests/regression/74-invalid_deref/16-uaf-packed-struct.c
similarity index 100%
rename from tests/regression/74-use_after_free/16-uaf-packed-struct.c
rename to tests/regression/74-invalid_deref/16-uaf-packed-struct.c
diff --git a/tests/regression/78-invalid-deref-scopes/01-scopes-no-static.c b/tests/regression/74-invalid_deref/17-scopes-no-static.c
similarity index 100%
rename from tests/regression/78-invalid-deref-scopes/01-scopes-no-static.c
rename to tests/regression/74-invalid_deref/17-scopes-no-static.c
diff --git a/tests/regression/74-use_after_free/01-simple-uaf.c b/tests/regression/74-invalid_deref/18-simple-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/01-simple-uaf.c
rename to tests/regression/74-invalid_deref/18-simple-uaf.c
diff --git a/tests/regression/77-mem-oob/02-oob-stack-simple.c b/tests/regression/74-invalid_deref/19-oob-stack-simple.c
similarity index 100%
rename from tests/regression/77-mem-oob/02-oob-stack-simple.c
rename to tests/regression/74-invalid_deref/19-oob-stack-simple.c
diff --git a/tests/regression/78-invalid-deref-scopes/02-scopes-global-var.c b/tests/regression/74-invalid_deref/20-scopes-global-var.c
similarity index 100%
rename from tests/regression/78-invalid-deref-scopes/02-scopes-global-var.c
rename to tests/regression/74-invalid_deref/20-scopes-global-var.c
diff --git a/tests/regression/77-mem-oob/03-oob-loop.c b/tests/regression/74-invalid_deref/21-oob-loop.c
similarity index 100%
rename from tests/regression/77-mem-oob/03-oob-loop.c
rename to tests/regression/74-invalid_deref/21-oob-loop.c
diff --git a/tests/regression/78-invalid-deref-scopes/03-scopes-static.c b/tests/regression/74-invalid_deref/22-scopes-static.c
similarity index 100%
rename from tests/regression/78-invalid-deref-scopes/03-scopes-static.c
rename to tests/regression/74-invalid_deref/22-scopes-static.c
diff --git a/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c b/tests/regression/74-invalid_deref/23-oob-deref-after-ptr-arith.c
similarity index 100%
rename from tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c
rename to tests/regression/74-invalid_deref/23-oob-deref-after-ptr-arith.c
diff --git a/tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c b/tests/regression/74-invalid_deref/24-uaf-free-in-wrapper-fun.c
similarity index 100%
rename from tests/regression/74-use_after_free/05-uaf-free-in-wrapper-fun.c
rename to tests/regression/74-invalid_deref/24-uaf-free-in-wrapper-fun.c
diff --git a/tests/regression/74-use_after_free/06-uaf-struct.c b/tests/regression/74-invalid_deref/25-uaf-struct.c
similarity index 100%
rename from tests/regression/74-use_after_free/06-uaf-struct.c
rename to tests/regression/74-invalid_deref/25-uaf-struct.c
diff --git a/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c b/tests/regression/74-invalid_deref/26-memset-memcpy-addr-offs.c
similarity index 100%
rename from tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c
rename to tests/regression/74-invalid_deref/26-memset-memcpy-addr-offs.c
diff --git a/tests/regression/74-use_after_free/11-wrapper-funs-uaf.c b/tests/regression/74-invalid_deref/27-wrapper-funs-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/11-wrapper-funs-uaf.c
rename to tests/regression/74-invalid_deref/27-wrapper-funs-uaf.c
diff --git a/tests/regression/74-use_after_free/12-multi-threaded-uaf.c b/tests/regression/74-invalid_deref/28-multi-threaded-uaf.c
similarity index 100%
rename from tests/regression/74-use_after_free/12-multi-threaded-uaf.c
rename to tests/regression/74-invalid_deref/28-multi-threaded-uaf.c
diff --git a/tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c b/tests/regression/74-invalid_deref/29-multi-threaded-uaf-with-joined-thread.c
similarity index 100%
rename from tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c
rename to tests/regression/74-invalid_deref/29-multi-threaded-uaf-with-joined-thread.c
diff --git a/tests/regression/75-invalid_dealloc/01-invalid-dealloc-simple.c b/tests/regression/75-invalid_free/01-invalid-dealloc-simple.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/01-invalid-dealloc-simple.c
rename to tests/regression/75-invalid_free/01-invalid-dealloc-simple.c
diff --git a/tests/regression/75-invalid_dealloc/02-invalid-dealloc-struct.c b/tests/regression/75-invalid_free/02-invalid-dealloc-struct.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/02-invalid-dealloc-struct.c
rename to tests/regression/75-invalid_free/02-invalid-dealloc-struct.c
diff --git a/tests/regression/75-invalid_dealloc/03-invalid-dealloc-array.c b/tests/regression/75-invalid_free/03-invalid-dealloc-array.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/03-invalid-dealloc-array.c
rename to tests/regression/75-invalid_free/03-invalid-dealloc-array.c
diff --git a/tests/regression/75-invalid_dealloc/04-invalid-realloc.c b/tests/regression/75-invalid_free/04-invalid-realloc.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/04-invalid-realloc.c
rename to tests/regression/75-invalid_free/04-invalid-realloc.c
diff --git a/tests/regression/75-invalid_dealloc/05-free-at-offset.c b/tests/regression/75-invalid_free/05-free-at-offset.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/05-free-at-offset.c
rename to tests/regression/75-invalid_free/05-free-at-offset.c
diff --git a/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c b/tests/regression/75-invalid_free/06-realloc-at-offset.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
rename to tests/regression/75-invalid_free/06-realloc-at-offset.c
diff --git a/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c b/tests/regression/75-invalid_free/07-free-at-struct-offset.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
rename to tests/regression/75-invalid_free/07-free-at-struct-offset.c
diff --git a/tests/regression/74-use_after_free/08-itc-no-double-free.c b/tests/regression/75-invalid_free/08-itc-no-double-free.c
similarity index 100%
rename from tests/regression/74-use_after_free/08-itc-no-double-free.c
rename to tests/regression/75-invalid_free/08-itc-no-double-free.c
diff --git a/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c b/tests/regression/75-invalid_free/09-juliet-invalid-dealloc-alloca.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c
rename to tests/regression/75-invalid_free/09-juliet-invalid-dealloc-alloca.c
diff --git a/tests/regression/75-invalid_dealloc/10-invalid-dealloc-union.c b/tests/regression/75-invalid_free/10-invalid-dealloc-union.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/10-invalid-dealloc-union.c
rename to tests/regression/75-invalid_free/10-invalid-dealloc-union.c
diff --git a/tests/regression/74-use_after_free/07-itc-double-free.c b/tests/regression/75-invalid_free/11-itc-double-free.c
similarity index 100%
rename from tests/regression/74-use_after_free/07-itc-double-free.c
rename to tests/regression/75-invalid_free/11-itc-double-free.c
diff --git a/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c b/tests/regression/75-invalid_free/12-realloc-at-struct-offset.c
similarity index 100%
rename from tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
rename to tests/regression/75-invalid_free/12-realloc-at-struct-offset.c
diff --git a/tests/regression/74-use_after_free/10-juliet-double-free.c b/tests/regression/75-invalid_free/13-juliet-double-free.c
similarity index 100%
rename from tests/regression/74-use_after_free/10-juliet-double-free.c
rename to tests/regression/75-invalid_free/13-juliet-double-free.c

From 7ebf97e9ef2f9167898f40bd304880d48f10cb08 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 15:38:49 +0300
Subject: [PATCH 091/104] Fix scripts/goblint-lib-modules.py

---
 scripts/goblint-lib-modules.py | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index 342f9a76bd..5f02271616 100755
--- a/scripts/goblint-lib-modules.py
+++ b/scripts/goblint-lib-modules.py
@@ -6,16 +6,20 @@
 
 src_root_path = Path("./src")
 
-goblint_lib_path = src_root_path / "goblint_lib.ml"
+goblint_lib_paths = [
+    src_root_path / "goblint_lib.ml",
+    src_root_path / "util" / "std" / "goblint_std.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)
+for goblint_lib_path in goblint_lib_paths:
+    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([
@@ -29,15 +33,21 @@
     "Mainspec",
 
     # libraries
+    "Goblint_std",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_sites",
     "Goblint_build_info",
+    "Dune_build_info",
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
     "SpecCore", # spec stuff
     "SpecUtil", # spec stuff
+
+    "ConfigVersion",
+    "ConfigProfile",
+    "ConfigOcaml",
 ])
 
 src_modules = set()

From 910a11f903e217efcc946d7d9d988c50575cd3ae Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 12 Oct 2023 14:50:36 +0200
Subject: [PATCH 092/104] Activate `cil.addNestedScopeAttr` when
 `memOutOfBounds` analysis is active

---
 src/maingoblint.ml                                         | 1 +
 tests/regression/74-invalid_deref/08-memset-memcpy-array.c | 7 ++++---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 97f35214be..b5998df2d1 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -135,6 +135,7 @@ let check_arguments () =
   if get_bool "allfuns" && not (get_bool "exp.earlyglobs") then (set_bool "exp.earlyglobs" true; warn "allfuns enables exp.earlyglobs.\n");
   if not @@ List.mem "escape" @@ get_string_list "ana.activated" then warn "Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!";
   if List.mem "malloc_null" @@ get_string_list "ana.activated" && not @@ get_bool "sem.malloc.fail" then (set_bool "sem.malloc.fail" true; warn "The malloc_null analysis enables sem.malloc.fail.");
+  if List.mem "memOutOfBounds" @@ get_string_list "ana.activated" && not @@ get_bool "cil.addNestedScopeAttr" then (set_bool "cil.addNestedScopeAttr" true; warn "The memOutOfBounds analysis enables cil.addNestedScopeAttr.");
   if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr");
   (* order matters: non-ptr=false, int=true -> int=false cascades to interval=false with warning *)
   if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int");
diff --git a/tests/regression/74-invalid_deref/08-memset-memcpy-array.c b/tests/regression/74-invalid_deref/08-memset-memcpy-array.c
index f231ba2dc4..210a61d459 100644
--- a/tests/regression/74-invalid_deref/08-memset-memcpy-array.c
+++ b/tests/regression/74-invalid_deref/08-memset-memcpy-array.c
@@ -6,13 +6,14 @@
 int main(int argc, char const *argv[]) {
     int arr[42]; // Size should be 168 bytes (with 4 byte ints)
     int *b = arr;
-    
+    int random;
+
 
     memset(b, 0, 168); //NOWARN
     memset(b, 0, sizeof(arr)); //NOWARN
     memset(b, 0, 169); //WARN
     memset(b, 0, sizeof(arr) + 1); //WARN
-    
+
     int *c = malloc(sizeof(arr)); // Size should be 168 bytes (with 4 byte ints)
     memcpy(b, c, 168); //NOWARN
     memcpy(b, c, sizeof(arr)); //NOWARN
@@ -26,7 +27,7 @@ int main(int argc, char const *argv[]) {
         memset(b, 0, 168); //WARN
         memcpy(b, c, 168); //WARN
     } else if (*(argv + 5)) {
-        int random = rand();
+        random = rand();
         b = &random;
         memset(b, 0, 168); //WARN
         memcpy(b, c, 168); //WARN

From fe369158efccfe1c531429f18e03b79b49dab38e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 14 Oct 2023 11:04:13 +0200
Subject: [PATCH 093/104] Add `AnalysisStateUtil` to `goblint_lib.ml` (#1201)

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

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index dadeb2cda1..a71a0c9684 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -23,6 +23,7 @@ module CfgTools = CfgTools
 module Analyses = Analyses
 module Constraints = Constraints
 module AnalysisState = AnalysisState
+module AnalysisStateUtil = AnalysisStateUtil
 module ControlSpecC = ControlSpecC
 
 (** Master control program (MCP) is the analysis specification for the dynamic product of activated analyses. *)

From a4261deb3f784720d0806cf92c1c9165d2cbe36e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 Oct 2023 17:36:23 +0300
Subject: [PATCH 094/104] Add final message for unknown ignored longjmp

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

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 21f3958a81..95a13ed516 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1663,7 +1663,8 @@ struct
         if M.tracing then Messages.tracel "longjmp" "Jumping to %a\n" JmpBufDomain.JmpBufSet.pretty targets;
         let handle_target target = match target with
           | JmpBufDomain.BufferEntryOrTop.AllTargets ->
-            M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env
+            M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env;
+            M.msg_final Error ~category:Unsound ~tags:[Category Imprecise; Category Call] "Longjmp to unknown target ignored"
           | Target (target_node, target_context) ->
             let target_fundec = Node.find_fundec target_node in
             if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (

From 5948ca4212df4c896ee20082a4eb6422c70bd06d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 Oct 2023 17:37:45 +0300
Subject: [PATCH 095/104] Mark longjmp-top reachability test as TODO

---
 tests/regression/68-longjmp/56-longjmp-top.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/68-longjmp/56-longjmp-top.c b/tests/regression/68-longjmp/56-longjmp-top.c
index 4d57b42fd3..adb3a47476 100644
--- a/tests/regression/68-longjmp/56-longjmp-top.c
+++ b/tests/regression/68-longjmp/56-longjmp-top.c
@@ -15,7 +15,7 @@ int main() {
     longjmp(*buf_ptr, 1); // NO CRASH: problem?!
   }
   else {
-    __goblint_check(1); // reachable
+    __goblint_check(1); // TODO reachable: https://github.com/goblint/analyzer/pull/1210#discussion_r1350021903
   }
   return 0;
 }

From 32be7d50615878bb400b6d665d5bb589be28b79c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 20 Oct 2023 13:39:23 +0300
Subject: [PATCH 096/104] Improve names of some global constraint variables

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

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index db75455b40..793978980b 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -84,7 +84,7 @@ struct
   module V =
   struct
     (* TODO: Either3? *)
-    include Printable.Either (Printable.Either (VMutex) (VMutexInits)) (VGlobal)
+    include Printable.Either (struct include Printable.Either (VMutex) (VMutexInits) let name () = "mutex" end) (VGlobal)
     let name () = "MutexGlobals"
     let mutex x: t = `Left (`Left x)
     let mutex_inits: t = `Left (`Right ())
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 95a13ed516..812d056de4 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1467,6 +1467,7 @@ struct
   module V =
   struct
     include Printable.Either (S.V) (Printable.Either (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C)))
+    let name () = "longjmp"
     let s x = `Left x
     let longjmpto x = `Right (`Left x)
     let longjmpret x = `Right (`Right x)

From af904ac55762f3b9bb59bce54a13ed8e311894d1 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Mon, 23 Oct 2023 20:19:25 +0000
Subject: [PATCH 097/104] Bump actions/setup-node from 3 to 4

Bumps [actions/setup-node](https://github.com/actions/setup-node) from 3 to 4.
- [Release notes](https://github.com/actions/setup-node/releases)
- [Commits](https://github.com/actions/setup-node/compare/v3...v4)

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

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

diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 007ea34619..65dfbe7bac 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -153,7 +153,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
index 1092606bc6..6c7360f9e3 100644
--- a/.github/workflows/metadata.yml
+++ b/.github/workflows/metadata.yml
@@ -39,7 +39,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
index 40652791fa..94c49e4bf6 100644
--- a/.github/workflows/options.yml
+++ b/.github/workflows/options.yml
@@ -18,7 +18,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

From 0cf9bc498741c24abda05007134c067f297a1b72 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 26 Oct 2023 10:28:06 +0300
Subject: [PATCH 098/104] Add smtprc-tid unsound case

---
 tests/regression/03-practical/32-smtprc-tid.c | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 tests/regression/03-practical/32-smtprc-tid.c

diff --git a/tests/regression/03-practical/32-smtprc-tid.c b/tests/regression/03-practical/32-smtprc-tid.c
new file mode 100644
index 0000000000..1d4810ee2e
--- /dev/null
+++ b/tests/regression/03-practical/32-smtprc-tid.c
@@ -0,0 +1,38 @@
+#include <pthread.h>
+#include <stdlib.h>
+
+int threads_total = 4;
+pthread_t *tids;
+
+void *cleaner(void *arg) {
+  while (1) {
+    for (int i = 0; i < threads_total; i++) {
+      if (tids[i]) { // RACE!
+        if (!pthread_join(tids[i], NULL)) // RACE!
+          tids[i] = 0; // RACE!
+      }
+    }
+  }
+  return NULL;
+}
+
+void *thread(int i) { // wrong argument type is important
+  tids[i] = pthread_self(); // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t tid;
+  tids = malloc(threads_total * sizeof(pthread_t));
+
+  for(int i = 0; i < threads_total; i++)
+    tids[i] = 0;
+
+  pthread_create(&tid, NULL, cleaner, NULL);
+
+  for(int i = 0; i < threads_total; i++) {
+    pthread_create(&tid, NULL, thread, (int *)i); // cast is important
+  }
+
+  return 0;
+}

From 2a958bd7e1a71c0216a0d49317796a45fd13ddf7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 20 Sep 2023 17:47:35 +0300
Subject: [PATCH 099/104] Fix smtprc-tid unsoundness

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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index caa2a41533..6536a9c496 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -399,6 +399,8 @@ struct
           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 ()))
+        | IndexPI | PlusPI ->
+          addToAddrOp p1 (AD.to_int p2) (* sometimes index is AD for some reason... *)
         | _ -> VD.top ()
       end
     (* For other values, we just give up! *)

From 6899d444f27c1f434ade07565ab5d23a631ea753 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 27 Oct 2023 15:10:48 +0300
Subject: [PATCH 100/104] Add --enable ana.sv-comp.functions to
 20-race-2_1-container_of.c

---
 tests/regression/10-synch/20-race-2_1-container_of.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/10-synch/20-race-2_1-container_of.c b/tests/regression/10-synch/20-race-2_1-container_of.c
index 6083cf4ca0..940649c43b 100644
--- a/tests/regression/10-synch/20-race-2_1-container_of.c
+++ b/tests/regression/10-synch/20-race-2_1-container_of.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] thread --set ana.path_sens[+] threadflag
+// PARAM: --set ana.activated[+] thread --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions
 #include <pthread.h>
 #include <stdio.h>
 #include <stdlib.h>
@@ -60,7 +60,7 @@ int my_drv_probe(struct my_data *data) {
 	ldv_assert(data->shared.a==0); // NORACE
 	ldv_assert(data->shared.b==0); // NORACE
 
-	int res = __VERIFIER_nondet_int();
+	int res = magic();
 	if(res)
 		goto exit;
 	//register callback

From 2c0a08f0e356d7e92fff2db874d081e38831e272 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 29 Oct 2023 20:14:11 +0200
Subject: [PATCH 101/104] Fix accident in 20 10 test

---
 tests/regression/10-synch/20-race-2_1-container_of.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/10-synch/20-race-2_1-container_of.c b/tests/regression/10-synch/20-race-2_1-container_of.c
index 940649c43b..04d5facbb7 100644
--- a/tests/regression/10-synch/20-race-2_1-container_of.c
+++ b/tests/regression/10-synch/20-race-2_1-container_of.c
@@ -60,7 +60,7 @@ int my_drv_probe(struct my_data *data) {
 	ldv_assert(data->shared.a==0); // NORACE
 	ldv_assert(data->shared.b==0); // NORACE
 
-	int res = magic();
+	int res = __VERIFIER_nondet_int();
 	if(res)
 		goto exit;
 	//register callback

From a2a4fa2be47c1f2fc2f3eff167c9e57db9e346ee Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 30 Oct 2023 17:11:28 +0200
Subject: [PATCH 102/104] Don't output trivial congruence invariant (closes
 #1218)

---
 src/cdomains/intDomain.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 748df62300..3bc84ae676 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -3274,6 +3274,7 @@ struct
 
   let invariant_ikind e ik x =
     match x with
+    | x when is_top x -> Invariant.top ()
     | Some (c, m) when m =: Ints_t.zero ->
       if get_bool "witness.invariant.exact" then
         let c = Ints_t.to_bigint c in

From 1cf3942190226126befdac561159c15758153a52 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 16:07:47 +0200
Subject: [PATCH 103/104] Make memsafety autotuner enable ana.arrayoob (PR
 #1201)

https://github.com/goblint/analyzer/pull/1201#issuecomment-1787126733
---
 src/autoTune.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 186d930189..b96848c841 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -218,6 +218,7 @@ let focusOnMemSafetySpecification () =
     enableAnalyses uafAna
   | ValidDeref -> (* Enable the memOutOfBounds analysis *)
     let memOobAna = ["memOutOfBounds"] in
+    set_bool "ana.arrayoob" true;
     print_endline "Setting \"cil.addNestedScopeAttr\" to true";
     set_bool "cil.addNestedScopeAttr" true;
     print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
@@ -232,6 +233,7 @@ let focusOnMemSafetySpecification () =
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
   | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
+    set_bool "ana.arrayoob" true;
     (print_endline "Setting \"cil.addNestedScopeAttr\" to true";
      set_bool "cil.addNestedScopeAttr" true;
      if (get_int "ana.malloc.unique_address_count") < 1 then (

From 6131273c1c95bf762749aa7a6a857fec09603def Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 16:10:14 +0200
Subject: [PATCH 104/104] Separate memsafetySpecification autotuner and enable
 in svcomp conf

Normal specification autotuner does other things we didn't want in SV-COMP.
---
 conf/svcomp.json                    | 3 ++-
 src/common/util/options.schema.json | 2 +-
 src/maingoblint.ml                  | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index 913d43784b..342ac6f298 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -70,7 +70,8 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic"
+        "loopUnrollHeuristic",
+        "memsafetySpecification"
       ]
     }
   },
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 400dde06dc..4d1b012701 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -544,7 +544,7 @@
               "type": "array",
               "items": { "type": "string" },
               "default": [
-                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds"
+                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification"
               ]
             }
           },
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index b5998df2d1..9e0b41fe3c 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -186,7 +186,7 @@ let handle_options () =
   check_arguments ();
   AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
-  if AutoTune.isActivated "specification" && get_string "ana.specification" <> "" then
+  if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then
     AutoTune.focusOnMemSafetySpecification ();
   Cilfacade.init_options ();
   handle_flags ()