diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 7b87d3ff51..908dc88401 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1043,10 +1043,24 @@ 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 (
+              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 (
+              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 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
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
@@ -2023,14 +2037,78 @@ 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
+      )
+    | _ ->
+      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, _) -> 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
@@ -2050,13 +2128,28 @@ 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 = 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 ->
+          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.top_of @@ Cilfacade.ptrdiff_ikind ()
+            end
+          in
+          Option.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
       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
@@ -2117,13 +2210,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))
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 8576096dfe..dbaa2d69fc 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)
 
@@ -19,15 +20,24 @@ 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 (
+      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"
+    )
 
   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 ->
+        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 *)
   let return ctx (exp:exp option) (f:fundec) : D.t =
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index c715a1d2e7..fc60352298 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -3,6 +3,7 @@
 open GoblintCil
 open Analyses
 open MessageCategory
+open AnalysisStateUtil
 
 module AS = AnalysisState
 module VDQ = ValueDomainQueries
@@ -88,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
@@ -117,8 +122,9 @@ struct
           | x::xs -> List.fold_left VDQ.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
+        (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
@@ -159,6 +165,50 @@ struct
         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 =
+      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) ->
+      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
     | a when not (VDQ.AD.is_top a) ->
@@ -174,22 +224,25 @@ 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
+                  | Addr (_, o) -> ID.is_top_of (Cilfacade.ptrdiff_ikind ()) (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 *)
-              (* 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 ->
@@ -197,18 +250,55 @@ struct
           ID.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;
       ID.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 *)
       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 =
+              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
+              | 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 ->
@@ -219,6 +309,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
@@ -229,10 +320,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
@@ -240,11 +331,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
@@ -275,6 +366,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
@@ -303,16 +395,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
@@ -320,11 +412,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
@@ -333,23 +425,24 @@ 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, _ ->
-      AnalysisState.svcomp_may_invalid_deref := true;
-      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
+      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 ptr 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;
-      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
+      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 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
     | `Lifted ds, `Lifted en ->
       let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
@@ -358,11 +451,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;
-          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
+          set_mem_safety_flag InvalidDeref;
+          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 ->
-          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
 
@@ -396,7 +489,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
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
@@ -412,4 +507,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 02231336c0..ef63ab3e91 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -3,6 +3,7 @@
 open GoblintCil
 open Analyses
 open MessageCategory
+open AnalysisStateUtil
 
 module AllocaVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All alloca() Variables" end)
 module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
@@ -14,7 +15,7 @@ module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted
 
 module Spec : Analyses.MCPSpec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "useAfterFree"
 
@@ -23,18 +24,11 @@ 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 _ _ = ()
 
 
   (* 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
 
@@ -70,23 +64,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 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
       | `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"
@@ -115,8 +109,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 ->
@@ -179,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
@@ -189,17 +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;
-    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]
-    )
+    (* 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)]
 
   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
@@ -251,9 +237,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 ()
 
diff --git a/src/autoTune.ml b/src/autoTune.ml
index d532081799..186d930189 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -210,6 +210,38 @@ let activateLongjmpAnalysesWhenRequired () =
     enableAnalyses longjmpAnalyses;
   )
 
+let focusOnMemSafetySpecification () =
+  match Svcomp.Specification.of_option () with
+  | ValidFree -> (* Enable the useAfterFree analysis *)
+    let uafAna = ["useAfterFree"] in
+    print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
+    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
+  | ValidMemcleanup -> (* Enable the memLeak analysis *)
+    let memLeakAna = ["memLeak"] in
+    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 *)
+    (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)
+  | _ -> ()
+
 let focusOnSpecification () =
   match Svcomp.Specification.of_option () with
   | UnreachCall s -> ()
@@ -219,13 +251,7 @@ let focusOnSpecification () =
   | 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) ^ "\"";
-    enableAnalyses uafAna
-  (* TODO: Finish these two below later *)
-  | ValidDeref
-  | ValidMemtrack -> ()
+  | _ -> ()
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
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 ()
 
diff --git a/src/common/framework/analysisState.ml b/src/common/framework/analysisState.ml
index ca619d4dfb..05a93741f8 100644
--- a/src/common/framework/analysisState.ml
+++ b/src/common/framework/analysisState.ml
@@ -13,9 +13,12 @@ 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 a memory leak occurred *)
+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/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 7f6116f604..ba57074e5a 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -40,7 +40,8 @@ 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";
+  Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr"
 
 let init () =
   initCIL ();
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 1b9c7d3fd5..400dde06dc 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/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
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 98363233a2..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");
@@ -185,6 +186,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 ()
 
diff --git a/src/util/analysisStateUtil.ml b/src/util/analysisStateUtil.ml
new file mode 100644
index 0000000000..a34be33f18
--- /dev/null
+++ b/src/util/analysisStateUtil.ml
@@ -0,0 +1,13 @@
+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
+    | 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 f1ee18ed72..22543d48a9 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -55,6 +55,8 @@ struct
         | ValidFree -> "valid-free"
         | 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 8dafb8873c..4a3da23d9b 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -9,10 +9,13 @@ type t =
   | ValidFree
   | 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 \\(.*\\)) )" 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
@@ -27,14 +30,19 @@ 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
+    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
+    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-free" then
-      ValidFree
-    else if global = "valid-deref" then
-      ValidDeref
-    else if global = "valid-memtrack" then
-      ValidMemtrack
+    if global = "valid-memcleanup" then
+      ValidMemcleanup
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
   else
@@ -65,5 +73,7 @@ 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 *)
+    | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index fb1604f03e..9f5a3c1801 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -505,14 +505,17 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree ->
+    | ValidFree
+    | ValidDeref
+    | ValidMemtrack
+    | MemorySafety ->
       let module TrivialArg =
       struct
         include Arg
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_free 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
@@ -523,37 +526,7 @@ 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)
-      )
-    | 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 (
+      ) else (
         let module TaskResult =
         struct
           module Arg = TrivialArg
@@ -565,14 +538,14 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidMemtrack ->
+    | ValidMemcleanup ->
       let module TrivialArg =
       struct
         include Arg
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_memtrack then
+      if not !AnalysisState.svcomp_may_invalid_memcleanup then (
         let module TaskResult =
         struct
           module Arg = Arg
@@ -583,7 +556,7 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      else (
+      ) else (
         let module TaskResult =
         struct
           module Arg = TrivialArg
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 94%
rename from tests/regression/77-mem-oob/07-memcpy-oob.c
rename to tests/regression/74-invalid_deref/07-memcpy-oob.c
index 012f92996e..5605404a87 100644
--- a/tests/regression/77-mem-oob/07-memcpy-oob.c
+++ b/tests/regression/74-invalid_deref/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
 
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 96%
rename from tests/regression/77-mem-oob/08-memset-memcpy-array.c
rename to tests/regression/74-invalid_deref/08-memset-memcpy-array.c
index f231ba2dc4..210a61d459 100644
--- a/tests/regression/77-mem-oob/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
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/74-invalid_deref/10-oob-two-loops.c b/tests/regression/74-invalid_deref/10-oob-two-loops.c
new file mode 100644
index 0000000000..303aac242e
--- /dev/null
+++ b/tests/regression/74-invalid_deref/10-oob-two-loops.c
@@ -0,0 +1,22 @@
+// 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] = rand(); //NOWARN
+	}
+
+	int *q = p;
+
+	while (*q >= 0 && q < p + 1048 * sizeof(int)) { //WARN
+		if (rand()) {
+			q++;
+		} else {
+			(*q)--; //WARN
+		}
+	}
+	free(p);
+	return 0;
+}
diff --git a/tests/regression/74-invalid_deref/11-address-offset-oob.c b/tests/regression/74-invalid_deref/11-address-offset-oob.c
new file mode 100644
index 0000000000..ba01a12873
--- /dev/null
+++ b/tests/regression/74-invalid_deref/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;
+}
diff --git a/tests/regression/74-invalid_deref/12-memcpy-oob-src.c b/tests/regression/74-invalid_deref/12-memcpy-oob-src.c
new file mode 100644
index 0000000000..0f3a609fbe
--- /dev/null
+++ b/tests/regression/74-invalid_deref/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);
+}
+
diff --git a/tests/regression/74-invalid_deref/13-mem-oob-packed-struct.c b/tests/regression/74-invalid_deref/13-mem-oob-packed-struct.c
new file mode 100644
index 0000000000..552cd1bb0b
--- /dev/null
+++ b/tests/regression/74-invalid_deref/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);
+}
+
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-invalid_deref/15-juliet-uaf-global-var.c b/tests/regression/74-invalid_deref/15-juliet-uaf-global-var.c
new file mode 100644
index 0000000000..cc9819950f
--- /dev/null
+++ b/tests/regression/74-invalid_deref/15-juliet-uaf-global-var.c
@@ -0,0 +1,22 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.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
diff --git a/tests/regression/74-invalid_deref/16-uaf-packed-struct.c b/tests/regression/74-invalid_deref/16-uaf-packed-struct.c
new file mode 100644
index 0000000000..e10aa28486
--- /dev/null
+++ b/tests/regression/74-invalid_deref/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
+}
+
diff --git a/tests/regression/74-invalid_deref/17-scopes-no-static.c b/tests/regression/74-invalid_deref/17-scopes-no-static.c
new file mode 100644
index 0000000000..e0c4b47b73
--- /dev/null
+++ b/tests/regression/74-invalid_deref/17-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/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/74-invalid_deref/20-scopes-global-var.c b/tests/regression/74-invalid_deref/20-scopes-global-var.c
new file mode 100644
index 0000000000..9491e1c574
--- /dev/null
+++ b/tests/regression/74-invalid_deref/20-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/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/74-invalid_deref/22-scopes-static.c b/tests/regression/74-invalid_deref/22-scopes-static.c
new file mode 100644
index 0000000000..c13b665c84
--- /dev/null
+++ b/tests/regression/74-invalid_deref/22-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;
+}
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_free/10-invalid-dealloc-union.c b/tests/regression/75-invalid_free/10-invalid-dealloc-union.c
new file mode 100644
index 0000000000..be1eaa056d
--- /dev/null
+++ b/tests/regression/75-invalid_free/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;
+}
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
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) )
+