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 01/76] 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 02/76] 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 03/76] 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 04/76] 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 05/76] 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 06/76] 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 07/76] 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 08/76] 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 09/76] 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 10/76] 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 11/76] 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 12/76] 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 13/76] 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 14/76] 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 15/76] 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 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 16/76] 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 17/76] 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 18/76] 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 19/76] 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 20/76] 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 21/76] 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 22/76] 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 23/76] 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 24/76] 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 25/76] 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 26/76] 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 27/76] 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 28/76] 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 29/76] 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 30/76] 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 31/76] 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 32/76] 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 33/76] 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 34/76] 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 35/76] 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 36/76] 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 37/76] 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 38/76] 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 39/76] 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 40/76] 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 41/76] 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 42/76] 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 43/76] 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 44/76] 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 45/76] 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 46/76] 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 47/76] 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 48/76] 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 49/76] 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 50/76] 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 51/76] 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 52/76] 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 53/76] 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 54/76] 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 55/76] 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 56/76] 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 57/76] 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 58/76] 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 59/76] 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 60/76] 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 61/76] 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 62/76] 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 63/76] 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 64/76] 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 65/76] 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 66/76] 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 67/76] 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 68/76] 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 69/76] 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 70/76] 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 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 71/76] 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 72/76] 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 73/76] 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 74/76] 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 75/76] 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 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 76/76] 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