diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index aac369fed3..c4fdd633d3 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -570,6 +570,8 @@ struct
     if M.tracing then M.traceu "reachability" "All reachable vars: %a\n" AD.pretty !visited;
     List.map AD.singleton (AD.elements !visited)
 
+  let reachable_vars ask args gs st = Timing.wrap "reachability" (reachable_vars ask args gs) st
+
   let drop_non_ptrs (st:CPA.t) : CPA.t =
     if CPA.is_top st then st else
       let rec replace_val = function
@@ -1097,20 +1099,15 @@ struct
     | Int x -> ValueDomain.ID.to_int x
     | _ -> None
 
-  let eval_funvar ctx fval: varinfo list =
-    let exception OnlyUnknown in
-    try
-      let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
-      if AD.mem Addr.UnknownPtr fp then begin
-        let others = AD.to_var_may fp in
-        if others = [] then raise OnlyUnknown;
-        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval;
-        dummyFunDec.svar :: others
-      end else
-        AD.to_var_may fp
-    with SetDomain.Unsupported _ | OnlyUnknown ->
-      M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval;
-      [dummyFunDec.svar]
+  let eval_funvar ctx fval: Queries.AD.t =
+    let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
+    if AD.is_top fp then (
+      if AD.cardinal fp = 1 then
+        M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval
+      else
+        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval
+    );
+    fp
 
   (** Evaluate expression as address.
       Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *)
@@ -1204,10 +1201,7 @@ struct
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
     | Q.EvalFunvar e ->
-      begin
-        let fs = eval_funvar ctx e in
-        List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
-      end
+      eval_funvar ctx e
     | Q.EvalJumpBuf e ->
       begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | Address jmp_buf ->
@@ -1247,17 +1241,26 @@ struct
       end
     | Q.EvalValue e ->
       eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
-    | Q.BlobSize e -> begin
+    | Q.BlobSize {exp = e; base_address = from_base_addr} -> begin
         let p = eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
         (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *)
         match p with
         | Address a ->
           (* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
+          (* If we're asking for the BlobSize from the base address, then don't check for offsets => we want to avoid getting bot *)
           if AD.exists (function
-              | Addr (v,o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset
+              | Addr (v,o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || (if not from_base_addr then o <> `NoOffset else false)
               | _ -> false) a then
             Queries.Result.bot q
           else (
+            (* If we need the BlobSize from the base address, then remove any offsets *)
+            let a =
+              if from_base_addr then AD.map (function
+                  | Addr (v, o) -> Addr (v, `NoOffset)
+                  | addr -> addr) a
+              else
+                a
+            in
             let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a  None in
             (* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *)
             (match r with
@@ -1270,6 +1273,7 @@ struct
         match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | Address a -> a
         | Bot -> Queries.Result.bot q (* TODO: remove *)
+        | Int i -> AD.of_int i
         | _ -> Queries.Result.top q
       end
     | Q.EvalThread e -> begin
@@ -1287,7 +1291,17 @@ struct
         | Address a ->
           let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
           let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
-          List.fold_left (AD.join) (AD.empty ()) addrs
+          let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
+          if AD.may_be_unknown a then
+            AD.add UnknownPtr addrs' (* add unknown back *)
+          else
+            addrs'
+        | Int i ->
+          begin match Cilfacade.typeOf e with
+            | t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *)
+            | _
+            | exception Cilfacade.TypeOfError _ -> AD.empty () (* avoid unknown pointer result for non-pointer expression *)
+          end
         | _ -> AD.empty ()
       end
     | Q.ReachableUkTypes e -> begin
@@ -2400,34 +2414,38 @@ struct
     in
     if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st
 
-  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : Q.LS.t) : store =
+  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store =
     let ask = (Analyses.ask_of_ctx ctx) in
-    Q.LS.fold (fun (v, o) st ->
-        if CPA.mem v fun_st.cpa then
-          let lval = Mval.Exp.to_cil (v,o) in
-          let address = eval_lv ask ctx.global st lval in
-          let lval_type = (AD.type_of address) in
-          if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Mval.Exp.pretty (v, o) d_type lval_type;
-          match (CPA.find_opt v (fun_st.cpa)), lval_type with
-          | None, _ -> st
-          (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
-          | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
-          (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
-          | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
-          | _, _ -> begin
-              let new_val = get ask ctx.global fun_st address None in
-              if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
-              let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
-              let partDep = Dep.find_opt v fun_st.deps in
-              match partDep with
-              | None -> st'
-              (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
-              | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
-                                                                match val_opt with
-                                                                | None -> accCPA
-                                                                | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
-            end
-        else st) tainted_lvs local_st
+    AD.fold (fun addr st ->
+        match addr with
+        | Addr.Addr (v,o) ->
+          if CPA.mem v fun_st.cpa then
+            let lval = Addr.Mval.to_cil (v,o) in
+            let address = eval_lv ask ctx.global st lval in
+            let lval_type = Addr.type_of addr in
+            if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Addr.Mval.pretty (v,o) d_type lval_type;
+            match (CPA.find_opt v (fun_st.cpa)), lval_type with
+            | None, _ -> st
+            (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
+            | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
+            (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
+            | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
+            | _, _ -> begin
+                let new_val = get ask ctx.global fun_st address None in
+                if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
+                let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
+                let partDep = Dep.find_opt v fun_st.deps in
+                match partDep with
+                | None -> st'
+                (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
+                | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
+                                                                  match val_opt with
+                                                                  | None -> accCPA
+                                                                  | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
+              end
+          else st
+        | _ -> st
+      ) tainted_lvs local_st
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
     let combine_one (st: D.t) (fun_st: D.t) =
@@ -2442,9 +2460,9 @@ struct
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
         let ask = (Analyses.ask_of_ctx ctx) in
         let tainted = f_ask.f Q.MayBeTainted in
-        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname Q.LS.pretty tainted;
+        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
         if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
-        if Q.LS.is_top tainted then
+        if AD.is_top tainted then
           let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
           let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa';
@@ -2459,7 +2477,10 @@ struct
           let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
           if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller';
           (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
-          let tainted = Q.LS.filter (fun (v, _) ->  not (CPA.mem v cpa_new)) tainted in
+          let tainted = AD.filter (function
+              | Addr.Addr (v,_) -> not (CPA.mem v cpa_new)
+              | _ -> false
+            ) tainted in
           let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty st_combined.cpa;
           { fun_st with cpa = st_combined.cpa }
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 1b92cb320d..db75455b40 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -60,14 +60,10 @@ struct
     ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
 
   let protected_vars (ask: Q.ask): varinfo list =
-    let module VS = Set.Make (CilType.Varinfo) in
-    Q.LS.fold (fun (v, _) acc ->
-        let m = ValueDomain.Addr.of_var v in (* TODO: don't ignore offsets *)
-        Q.LS.fold (fun l acc ->
-            VS.add (fst l) acc (* always `NoOffset from mutex analysis *)
-          ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
-      ) (ask.f Q.MustLockset) VS.empty
-    |> VS.elements
+    Q.AD.fold (fun m acc ->
+        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
+      ) (ask.f Q.MustLockset) (Q.VS.empty ())
+    |> Q.VS.elements
 end
 
 module MutexGlobals =
@@ -126,10 +122,8 @@ struct
     if !AnalysisState.global_initialization then
       Lockset.empty ()
     else
-      let ls = ask.f Queries.MustLockset in
-      Q.LS.fold (fun (var, offs) acc ->
-          Lockset.add (Lock.of_mval (var, Lock.Offs.of_exp offs)) acc
-        ) ls (Lockset.empty ())
+      let ad = ask.f Queries.MustLockset in
+      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: use AD as Lockset *)
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 94de4fbf82..5f9f6f90f9 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -126,31 +126,10 @@ type t = {
   attrs: attr list; (** Attributes of function. *)
 }
 
-let special_of_old classify_name = fun args ->
-  match classify_name args with
-  | `Malloc e -> Malloc e
-  | `Calloc (count, size) -> Calloc { count; size; }
-  | `Realloc (ptr, size) -> Realloc { ptr; size; }
-  | `Lock (try_, write, return_on_success) ->
-    begin match args with
-      | [lock] -> Lock { lock ; try_; write; return_on_success; }
-      | [] -> failwith "lock has no arguments"
-      | _ -> failwith "lock has multiple arguments"
-    end
-  | `Unlock ->
-    begin match args with
-      | [arg] -> Unlock arg
-      | [] -> failwith "unlock has no arguments"
-      | _ -> failwith "unlock has multiple arguments"
-    end
-  | `ThreadCreate (thread, start_routine, arg) -> ThreadCreate { thread; start_routine; arg; }
-  | `ThreadJoin (thread, ret_var) -> ThreadJoin { thread; ret_var; }
-  | `Unknown _ -> Unknown
-
-let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old) (classify_name): t = {
+let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old): t = {
   attrs;
   accs = Accesses.of_old old_accesses;
-  special = special_of_old classify_name;
+  special = fun _ -> Unknown;
 }
 
 module MathPrintable = struct
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index b12da8230b..034fd6bb97 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -12,9 +12,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; });
     ("__builtin_memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; });
     ("__builtin___memset_chk", special [__ "dest" [w]; __ "ch" []; __ "count" []; drop "os" []] @@ fun dest ch count -> Memset { dest; ch; count; });
-    ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
+    ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); (* TODO: use n *)
     ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
     ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
+    ("memccpy", special [__ "dest" [w]; __ "src" [r]; drop "c" []; drop "n" []] @@ fun dest src -> Memcpy {dest; src}); (* C23 *) (* TODO: use n and c *)
     ("memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src });
     ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src });
     ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; drop "count" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
@@ -64,6 +65,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; });
     ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; });
     ("malloc", special [__ "size" []] @@ fun size -> Malloc size);
+    ("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size});
     ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size });
     ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr);
     ("abort", special [] Abort);
@@ -117,12 +119,14 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]; drop "wc" []; drop "ps" [r_deep; w_deep]]);
     ("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]);
     ("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]);
+    ("mbstowcs", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]);
     ("abs", unknown [drop "j" []]);
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
+    ("atexit", unknown [drop "function" [s]]);
   ]
 
 (** C POSIX library functions.
@@ -246,6 +250,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("timer_gettime", unknown [drop "timerid" []; drop "curr_value" [w_deep]]);
     ("timer_getoverrun", unknown [drop "timerid" []]);
     ("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]);
+    ("fstat", unknown [drop "fd" []; drop "buf" [w]]);
+    ("fstatat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "buf" [w]; drop "flags" []]);
     ("getpwnam", unknown [drop "name" [r]]);
     ("chdir", unknown [drop "path" [r]]);
     ("closedir", unknown [drop "dirp" [r]]);
@@ -292,12 +298,32 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *)
     ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
     ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]);
+    ("dprintf", unknown (drop "fd" [] :: drop "format" [r] :: VarArgs (drop' [r])));
+    ("vdprintf", unknown [drop "fd" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("mkdtemp", unknown [drop "template" [r; w]]);
+    ("mkstemp", unknown [drop "template" [r; w]]);
+    ("regcomp", unknown [drop "preg" [w_deep]; drop "regex" [r]; drop "cflags" []]);
+    ("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]);
+    ("regfree", unknown [drop "preg" [f_deep]]);
+    ("ffs", unknown [drop "i" []]);
+    ("_exit", special [drop "status" []] Abort);
+    ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]);
+    ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]);
+    ("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]);
+    ("wcswidth", unknown [drop "s" [r]; drop "n" []]);
+    ("link", unknown [drop "oldpath" [r]; drop "newpath" [r]]);
+    ("renameat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]]);
+    ("posix_fadvise", unknown [drop "fd" []; drop "offset" []; drop "len" []; drop "advice" []]);
+    ("getppid", unknown []);
+    ("lockf", unknown [drop "fd" []; drop "cmd" []; drop "len" []]);
   ]
 
 (** Pthread functions. *)
 let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
+    ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
+    ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
     ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
     ("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
     ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond);
@@ -322,16 +348,16 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
     ("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [r]]);
     ("pthread_rwlock_destroy", unknown [drop "rwlock" [f]]);
-    ("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true});
-    ("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true});
-    ("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true});
+    ("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = false});
+    ("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = false; return_on_success = false});
+    ("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false});
     ("pthread_rwlock_trywrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = true; return_on_success = false});
     ("pthread_rwlock_unlock", special [__ "rwlock" []] @@ fun rwlock -> Unlock rwlock);
     ("pthread_rwlockattr_init", unknown [drop "attr" [w]]);
     ("pthread_rwlockattr_destroy", unknown [drop "attr" [f]]);
     ("pthread_spin_init", unknown [drop "lock" [w]; drop "pshared" []]);
     ("pthread_spin_destroy", unknown [drop "lock" [f]]);
-    ("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true});
+    ("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false});
     ("pthread_spin_trylock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = true; write = true; return_on_success = false});
     ("pthread_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock);
     ("pthread_attr_init", unknown [drop "attr" [w]]);
@@ -412,6 +438,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);
+    ("__builtin_alloca", special [__ "size" []] @@ fun size -> Malloc size);
   ]
 
 let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -454,6 +481,11 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *)
     ("mempcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
     ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
+    ("rawmemchr", unknown [drop "s" [r]; drop "c" []]);
+    ("memrchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]);
+    ("memmem", unknown [drop "haystack" [r]; drop "haystacklen" []; drop "needle" [r]; drop "needlelen" [r]]);
+    ("getifaddrs", unknown [drop "ifap" [w]]);
+    ("freeifaddrs", unknown [drop "ifa" [f_deep]]);
   ]
 
 let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -470,6 +502,12 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__xpg_basename", unknown [drop "path" [r]]);
     ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *)
     ("madvise", unknown [drop "addr" []; drop "length" []; drop "advice" []]);
+    ("inotify_init1", unknown [drop "flags" []]);
+    ("inotify_add_watch", unknown [drop "fd" []; drop "pathname" [r]; drop "mask" []]);
+    ("inotify_rm_watch", unknown [drop "fd" []; drop "wd" []]);
+    ("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *)
+    ("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]);
+    ("fts_close", unknown [drop "ftsp" [f_deep]]);
   ]
 
 let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
@@ -530,6 +568,10 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__cmpxchg_wrong_size", special [] Abort);
     ("__xadd_wrong_size", special [] Abort);
     ("__put_user_bad", special [] Abort);
+    ("kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size);
+    ("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size);
+    ("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size});
+    ("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp);
   ]
 
 (** Goblint functions. *)
@@ -801,10 +843,14 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wattrset", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []]);
     ("endwin", unknown []);
     ("wgetch", unknown [drop "win" [r_deep; w_deep]]);
+    ("wget_wch", unknown [drop "win" [r_deep; w_deep]; drop "wch" [w]]);
+    ("unget_wch", unknown [drop "wch" []]);
     ("wmove", unknown [drop "win" [r_deep; w_deep]; drop "y" []; drop "x" []]);
     ("waddch", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
+    ("waddnstr", unknown [drop "win" [r_deep; w_deep]; drop "str" [r]; drop "n" []]);
     ("waddnwstr", unknown [drop "win" [r_deep; w_deep]; drop "wstr" [r]; drop "n" []]);
     ("wattr_on", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []; drop "opts" []]); (* opts argument currently not used *)
+    ("wattr_off", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []; drop "opts" []]); (* opts argument currently not used *)
     ("wrefresh", unknown [drop "win" [r_deep; w_deep]]);
     ("mvprintw", unknown (drop "win" [r_deep; w_deep] :: drop "y" [] :: drop "x" [] :: drop "fmt" [r] :: VarArgs (drop' [r])));
     ("initscr", unknown []);
@@ -813,10 +859,19 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("start_color", unknown []);
     ("use_default_colors", unknown []);
     ("wclear", unknown [drop "win" [r_deep; w_deep]]);
+    ("wclrtoeol", unknown [drop "win" [r_deep; w_deep]]);
     ("can_change_color", unknown []);
     ("init_color", unknown [drop "color" []; drop "red" []; drop "green" []; drop "blue" []]);
     ("init_pair", unknown [drop "pair" []; drop "f" [r]; drop "b" [r]]);
     ("wbkgd", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
+    ("keyname", unknown [drop "c" []]);
+    ("newterm", unknown [drop "type" [r]; drop "outfd" [r_deep; w_deep]; drop "infd" [r_deep; w_deep]]);
+    ("cbreak", unknown []);
+    ("nonl", unknown []);
+    ("keypad", unknown [drop "win" [r_deep; w_deep]; drop "bf" []]);
+    ("set_escdelay", unknown [drop "size" []]);
+    ("printw", unknown (drop "fmt" [r] :: VarArgs (drop' [r])));
+    ("werase", unknown [drop "win" [r_deep; w_deep]]);
   ]
 
 let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -868,46 +923,6 @@ let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t
 let reset_lazy () =
   ResettableLazy.reset activated_library_descs
 
-type categories = [
-  | `Malloc       of exp
-  | `Calloc       of exp * exp
-  | `Realloc      of exp * exp
-  | `Lock         of bool * bool * bool  (* try? * write? * return  on success *)
-  | `Unlock
-  | `ThreadCreate of exp * exp * exp (* id * f  * x       *)
-  | `ThreadJoin   of exp * exp (* id * ret_var *)
-  | `Unknown      of string ]
-
-
-let classify fn exps: categories =
-  let strange_arguments () =
-    M.warn ~category:Program "%s arguments are strange!" fn;
-    `Unknown fn
-  in
-  match fn with
-  | "pthread_join" ->
-    begin match exps with
-      | [id; ret_var] -> `ThreadJoin (id, ret_var)
-      | _ -> strange_arguments ()
-    end
-  | "kmalloc" | "__kmalloc" | "usb_alloc_urb" | "__builtin_alloca" ->
-    begin match exps with
-      | size::_ -> `Malloc size
-      | _ -> strange_arguments ()
-    end
-  | "kzalloc" ->
-    begin match exps with
-      | size::_ -> `Calloc (Cil.one, size)
-      | _ -> strange_arguments ()
-    end
-  | "calloc" ->
-    begin match exps with
-      | n::size::_ -> `Calloc (n, size)
-      | _ -> strange_arguments ()
-    end
-  | x -> `Unknown x
-
-
 module Invalidate =
 struct
   [@@@warning "-unused-value-declaration"] (* some functions are not used below *)
@@ -1036,7 +1051,6 @@ let invalidate_actions = [
     "sigaddset", writesAll;(*unsafe*)
     "raise", writesAll;(*unsafe*)
     "_strlen", readsAll;(*safe*)
-    "__builtin_alloca", readsAll;(*safe*)
     "dlopen", readsAll;(*safe*)
     "dlsym", readsAll;(*safe*)
     "dlclose", readsAll;(*safe*)
@@ -1197,7 +1211,7 @@ let is_safe_uncalled fn_name =
   List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex
 
 
-let unknown_desc ~f name = (* TODO: remove name argument, unknown function shouldn't have classify *)
+let unknown_desc f =
   let old_accesses (kind: AccessKind.t) args = match kind with
     | Write when GobConfig.get_bool "sem.unknown_function.invalidate.args" -> args
     | Write -> []
@@ -1215,18 +1229,12 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
     else
       []
   in
-  let classify_name args =
-    match classify name args with
-    | `Unknown _ as category ->
-      (* TODO: remove hack when all classify are migrated *)
-      if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
-        M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
-        M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
-      );
-      category
-    | category -> category
-  in
-  LibraryDesc.of_old ~attrs old_accesses classify_name
+  (* TODO: remove hack when all classify are migrated *)
+  if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
+    M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
+    M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
+  );
+  LibraryDesc.of_old ~attrs old_accesses
 
 let find f =
   let name = f.vname in
@@ -1235,9 +1243,9 @@ let find f =
   | None ->
     match get_invalidate_action name with
     | Some old_accesses ->
-      LibraryDesc.of_old old_accesses (classify name)
+      LibraryDesc.of_old old_accesses
     | None ->
-      unknown_desc ~f name
+      unknown_desc f
 
 
 let is_special fv =
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
new file mode 100644
index 0000000000..94c16e9c94
--- /dev/null
+++ b/src/analyses/memOutOfBounds.ml
@@ -0,0 +1,362 @@
+(** An analysis for the detection of out-of-bounds memory accesses ([memOutOfBounds]).*)
+
+open GoblintCil
+open Analyses
+open MessageCategory
+
+module AS = AnalysisState
+module VDQ = ValueDomainQueries
+
+(*
+  Note:
+  * This functionality is implemented as an analysis solely for the sake of maintaining
+    separation of concerns, as well as for having the ablility to conveniently turn it on or off
+  * It doesn't track any internal state
+*)
+module Spec =
+struct
+  include Analyses.IdentitySpec
+
+  module D = Lattice.Unit
+  module C = D
+
+  let context _ _ = ()
+
+  let name () = "memOutOfBounds"
+
+  (* HELPER FUNCTIONS *)
+
+  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 _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> false
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
+    | UnOp (_, e, _)
+    | CastE (_, e) -> exp_contains_a_ptr e
+    | BinOp (_, e1, e2, _) ->
+      exp_contains_a_ptr e1 || exp_contains_a_ptr e2
+    | Question (e1, e2, e3, _) ->
+      exp_contains_a_ptr e1 || exp_contains_a_ptr e2 || exp_contains_a_ptr e3
+    | Lval lval
+    | AddrOf lval
+    | StartOf lval -> lval_contains_a_ptr lval
+
+  and lval_contains_a_ptr (lval:lval) =
+    let (host, offset) = lval in
+    let host_contains_a_ptr = function
+      | Var v -> isPointerType v.vtype
+      | Mem e -> exp_contains_a_ptr e
+    in
+    let rec offset_contains_a_ptr = function
+      | NoOffset -> false
+      | Index (e, o) -> exp_contains_a_ptr e || offset_contains_a_ptr o
+      | Field (f, o) -> isPointerType f.ftype || offset_contains_a_ptr o
+    in
+    host_contains_a_ptr host || offset_contains_a_ptr offset
+
+  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 =
+    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 = (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)
+                    | `Bot -> VDQ.ID.bot ()
+                    | `Top -> VDQ.ID.top ()
+                  end
+                | _ ->
+                  let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in
+                  `Lifted (intdom_of_int type_size_in_bytes)
+              end
+            | _ -> VDQ.ID.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
+          | [] -> VDQ.ID.bot ()
+          | [x] -> x
+          | x::xs -> List.fold_left (fun acc elem ->
+              if VDQ.ID.compare acc elem >= 0 then elem else acc
+            ) x xs
+        end
+      | _ ->
+        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 =
+    match ptr_typ with
+    | TPtr (t, _) -> Some t
+    | _ -> None
+
+  let size_of_type_in_bytes typ =
+    let typ_size_in_bytes = (bitsSizeOf typ) / 8 in
+    intdom_of_int typ_size_in_bytes
+
+  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)
+    | `Top -> `Top
+    | `Bot -> `Bot
+
+  let rec offs_to_idx 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 = offs_to_idx field.ftype o in
+      IntDomain.IntDomTuple.add bytes_offset remaining_offset
+    | `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
+
+  let rec get_addr_offs ctx ptr =
+    match ctx.ask (Queries.MayPointTo ptr) with
+    | a when not (VDQ.AD.is_top a) ->
+      let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr in
+      begin match ptr_deref_type with
+        | Some t ->
+          begin match VDQ.AD.is_empty a with
+            | true ->
+              M.warn "Pointer %a has an empty points-to-set" d_exp ptr;
+              IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
+            | false ->
+              if VDQ.AD.exists (function
+                  | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o
+                  | _ -> false
+                ) a then (
+                (* TODO: Uncomment once staging-memsafety branch changes are applied *)
+                (* 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) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o
+                  | _ -> false
+                ) a then (
+                (* TODO: Uncomment once staging-memsafety branch changes are applied *)
+                (* 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
+                | _ -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()
+              end
+          end
+        | None ->
+          M.error "Expression %a doesn't have pointer type" d_exp ptr;
+          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;
+      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 ()
+    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, _), _ ->
+        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 ->
+            check_binop_exp ctx binop e1 e2 t;
+            check_exp_for_oob_access ctx ~is_implicitly_derefed e1;
+            check_exp_for_oob_access ctx ~is_implicitly_derefed e2
+          | _ -> check_exp_for_oob_access ctx ~is_implicitly_derefed e
+        end
+
+  and check_no_binop_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
+    let addr_offs = get_addr_offs ctx lval_exp in
+    let ptr_type = typeOf lval_exp in
+    let ptr_contents_type = get_ptr_deref_type ptr_type in
+    match ptr_contents_type with
+    | Some t ->
+      begin match VDQ.ID.is_top ptr_size with
+        | true ->
+          AS.svcomp_may_invalid_deref := true;
+          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;
+            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
+    | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp
+
+  and check_exp_for_oob_access ctx ?(is_implicitly_derefed = false) exp =
+    match exp with
+    | Const _
+    | SizeOf _
+    | SizeOfStr _
+    | AlignOf _
+    | AddrOfLabel _ -> ()
+    | Real e
+    | Imag e
+    | SizeOfE e
+    | AlignOfE e
+    | UnOp (_, e, _)
+    | CastE (_, e) -> check_exp_for_oob_access ctx ~is_implicitly_derefed e
+    | BinOp (bop, e1, e2, t) ->
+      check_exp_for_oob_access ctx ~is_implicitly_derefed e1;
+      check_exp_for_oob_access ctx ~is_implicitly_derefed e2
+    | Question (e1, e2, e3, _) ->
+      check_exp_for_oob_access ctx ~is_implicitly_derefed e1;
+      check_exp_for_oob_access ctx ~is_implicitly_derefed e2;
+      check_exp_for_oob_access ctx ~is_implicitly_derefed e3
+    | Lval lval
+    | StartOf lval
+    | AddrOf lval -> check_lval_for_oob_access ctx ~is_implicitly_derefed lval
+
+  and check_binop_exp ctx binop e1 e2 t =
+    let binopexp = BinOp (binop, e1, e2, t) in
+    let behavior = Undefined MemoryOutOfBoundsAccess in
+    let cwe_number = 823 in
+    match binop with
+    | PlusPI
+    | IndexPI
+    | MinusPI ->
+      let ptr_size = get_size_of_ptr_target ctx e1 in
+      let addr_offs = get_addr_offs ctx e1 in
+      let ptr_type = typeOf e1 in
+      let ptr_contents_type = get_ptr_deref_type ptr_type in
+      begin match ptr_contents_type with
+        | Some t ->
+          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)
+            | `Top -> `Top
+            | `Bot -> `Bot
+          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;
+              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;
+              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;
+                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
+        | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp
+      end
+    | _ -> ()
+
+
+  (* TRANSFER FUNCTIONS *)
+
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    check_lval_for_oob_access ctx lval;
+    check_exp_for_oob_access ctx rval;
+    ctx.local
+
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    check_exp_for_oob_access ctx exp;
+    ctx.local
+
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    Option.iter (fun x -> check_exp_for_oob_access ctx x) exp;
+    ctx.local
+
+  let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let desc = LibraryFunctions.find f in
+    let is_arg_implicitly_derefed arg =
+      let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in
+      let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in
+      let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in
+      let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in
+      List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args
+    in
+    Option.iter (fun x -> check_lval_for_oob_access ctx x) lval;
+    List.iter (fun arg -> check_exp_for_oob_access ctx ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist;
+    ctx.local
+
+  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    List.iter (fun arg -> check_exp_for_oob_access ctx arg) args;
+    [ctx.local, ctx.local]
+
+  let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t =
+    Option.iter (fun x -> check_lval_for_oob_access ctx x) lval;
+    ctx.local
+
+  let startstate v = ()
+  let exitstate v = ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 0375bd3f74..5dae8748cb 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -23,29 +23,23 @@ struct
     (* Only checks for v.vglob on purpose, acessing espaced locals after longjmp is UB like for any local *)
     not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static
 
-  let relevants_from_ls ls =
-    if Queries.LS.is_top ls then
-      VS.top ()
-    else
-      Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())
-
-  let relevants_from_ad ad =
+  let relevants_from_ad ls =
     (* TODO: what about AD with both known and unknown pointers? *)
-    if Queries.AD.is_top ad then
+    if Queries.AD.is_top ls then
       VS.top ()
     else
-      Queries.AD.fold (fun addr vs ->
+      Queries.AD.fold (fun addr acc ->
           match addr with
-          | Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs
-          | _ -> vs
-        ) ad (VS.empty ())
+          | Queries.AD.Addr.Addr (v, _) when is_relevant v -> VS.add v acc
+          | _ -> acc
+        ) ls (VS.empty ())
 
   (* transfer functions *)
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
+    let taintedcallee = relevants_from_ad (f_ask.f Queries.MayBeTainted) in
     add_to_all_defined taintedcallee ctx.local
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 7d8298a0a4..5a61976ef5 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -233,21 +233,15 @@ struct
       Mutexes.leq mutex_lockset protecting
     | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
-      let ls = Mutexes.fold (fun addr ls ->
-          match Addr.to_mval addr with
-          | Some (var, offs) -> Queries.LS.add (var, Addr.Offs.to_exp offs) ls
-          | None -> ls
-        ) held_locks (Queries.LS.empty ())
-      in
-      ls
+      Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ())
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks
     | Queries.MustProtectedVars {mutex = m; write} ->
       let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
       VarSet.fold (fun v acc ->
-          Queries.LS.add (v, `NoOffset) acc
-        ) protected (Queries.LS.empty ())
+          Queries.VS.add v acc
+        ) protected (Queries.VS.empty ())
     | Queries.IterSysVars (Global g, f) ->
       f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *)
     | WarnGlobal g ->
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 1bd4b6d544..acd687835e 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -15,12 +15,16 @@ struct
 
   let context _ _ = ()
 
-  let check_mval tainted ((v, offset): Queries.LS.elt) =
-    if not v.vglob && VS.mem v tainted then
-      M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
+  let check_mval tainted (addr: Queries.AD.elt) =
+    match addr with
+    | Queries.AD.Addr.Addr (v,_) ->
+      if not v.vglob && VS.mem v tainted then
+        M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
+    | _ -> ()
 
-  let rem_mval tainted ((v, offset): Queries.LS.elt) = match offset with
-    | `NoOffset -> VS.remove v tainted
+  let rem_mval tainted (addr: Queries.AD.elt) =
+    match addr with
+    | Queries.AD.Addr.Addr (v,`NoOffset) -> VS.remove v tainted
     | _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
 
 
@@ -88,11 +92,8 @@ struct
         | ad when Queries.AD.is_top ad && not (VS.is_empty octx.local) ->
           M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
         | ad ->
-          Queries.AD.iter (function
-              (* Use original access state instead of current with removed written vars. *)
-              | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (v, ValueDomain.Offs.to_exp o)
-              | _ -> ()
-            ) ad
+          (* Use original access state instead of current with removed written vars. *)
+          Queries.AD.iter (check_mval octx.local) ad
       end;
       ctx.local
     | Access {ad; kind = Write; _} ->
@@ -102,9 +103,7 @@ struct
           ctx.local
         | ad ->
           Queries.AD.fold (fun addr vs ->
-              match addr with
-              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
-              | _ -> vs
+              rem_mval vs addr
             ) ad ctx.local
       end
     | _ -> ctx.local
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index d053cd103b..feb9599977 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -6,31 +6,19 @@
 open GoblintCil
 open Analyses
 
-module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)
-
-let to_mvals ad =
-  (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
-  Queries.AD.fold (fun addr mvals ->
-      match addr with
-      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals (* TODO: use unconverted addrs in domain? *)
-      | _ -> mvals
-    ) ad (D.empty ())
+module AD = ValueDomain.AD
 
 module Spec =
 struct
   include Analyses.IdentitySpec
 
   let name () = "taintPartialContexts"
-  module D = D
+  module D = AD
   module C = Lattice.Unit
 
   (* Add Lval or any Lval which it may point to to the set *)
   let taint_lval ctx (lval:lval) : D.t =
-    let d = ctx.local in
-    (match lval with
-     | (Var v, offs) -> D.add (v, Offset.Exp.of_cil offs) d
-     | (Mem e, _) -> D.union (to_mvals (ctx.ask (Queries.MayPointTo e))) d
-    )
+    D.union (ctx.ask (Queries.MayPointTo (AddrOf lval))) ctx.local
 
   (* this analysis is context insensitive*)
   let context _ _ = ()
@@ -45,14 +33,12 @@ struct
     let d_return =
       if D.is_top d then
         d
-      else (
+      else
         let locals = f.sformals @ f.slocals in
-        D.filter (fun (v, _) ->
-            not (List.exists (fun local ->
-                CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
-              ) locals)
+        D.filter (function
+            | AD.Addr.Addr (v,_) -> not (List.exists (fun local -> CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))) locals)
+            | _ -> false
           ) d
-      )
     in
     if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return;
     d_return
@@ -94,9 +80,10 @@ struct
       else
         deep_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.MayPointTo addr)))) d shallow_addrs
+    (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
+    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.MayPointTo addr))) d shallow_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.ReachableFrom addr)))) d deep_addrs
+    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.ReachableFrom addr))) d deep_addrs
     in
     d
 
@@ -111,7 +98,7 @@ struct
 
   let query ctx (type a) (q: a Queries.t) : a Queries.result =
     match q with
-    | MayBeTainted -> (ctx.local : Queries.LS.t)
+    | MayBeTainted -> (ctx.local : Queries.AD.t)
     | _ -> Queries.Result.top q
 
 end
@@ -122,5 +109,8 @@ let _ =
 module VS = SetDomain.ToppedSet(Basetype.Variables) (struct let topname = "All" end)
 
 (* Convert Lval set to (less precise) Varinfo set. *)
-let conv_varset (lval_set : Spec.D.t) : VS.t =
-  if Spec.D.is_top lval_set then VS.top () else VS.of_list (List.map (fun (v, _) -> v) (Spec.D.elements lval_set))
+let conv_varset (addr_set : Spec.D.t) : VS.t =
+  if Spec.D.is_top addr_set then
+    VS.top ()
+  else
+    VS.of_list (Spec.D.to_var_may addr_set)
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 634a684c7c..dcd49c9f02 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -437,10 +437,14 @@ struct
     let d_local =
       (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
          TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
-      if Queries.LS.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
+      if Queries.AD.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
         D.top ()
       else
-        let taint_exp = Queries.ES.of_list (List.map Mval.Exp.to_cil_exp (Queries.LS.elements tainted)) in
+        let taint_exp =
+          Queries.AD.to_mval tainted
+          |> List.map Addr.Mval.to_cil_exp
+          |> Queries.ES.of_list
+        in
         D.filter (fun exp -> not (Queries.ES.mem exp taint_exp)) ctx.local
     in
     let d = D.meet au d_local in
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 0de5afc32c..4bc97b34ab 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -7,7 +7,7 @@ module IdxDom = ValueDomain.IndexDomain
 
 open GoblintCil
 
-module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO HoareDomain? *)
+module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO: AD? *)
 module Simple = Lattice.Reverse (Mutexes)
 module Priorities = IntDomain.Lifted
 
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 0388ce2995..1a7ec2276d 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -80,19 +80,21 @@ type _ t =
   | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *)
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
-  | MustLockset: LS.t t
+  | MustLockset: AD.t t
   | MustBeAtomic: MustBool.t t
   | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
   | MustBeUniqueThread: MustBool.t t
   | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t
   | ThreadCreateIndexedNode: ThreadNodeLattice.t t
   | MayBeThreadReturn: MayBool.t t
-  | EvalFunvar: exp -> LS.t t
+  | EvalFunvar: exp -> AD.t t
   | EvalInt: exp -> ID.t t
   | EvalStr: exp -> SD.t t
   | EvalLength: exp -> ID.t t (* length of an array or string *)
   | EvalValue: exp -> VD.t t
-  | BlobSize: exp -> ID.t t (* size of a dynamically allocated `Blob pointed to by exp *)
+  | BlobSize: {exp: Cil.exp; base_address: bool} -> ID.t t
+  (* Size of a dynamically allocated `Blob pointed to by exp. *)
+  (* If the record's second field is set to true, then address offsets are discarded and the size of the `Blob is asked for the base address. *)
   | CondVars: exp -> ES.t t
   | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *)
   | IterPrevVars: iterprevvar -> Unit.t t
@@ -114,13 +116,13 @@ type _ t =
   | CreatedThreads: ConcDomain.ThreadSet.t t
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
-  | MustProtectedVars: mustprotectedvars -> LS.t t
+  | MustProtectedVars: mustprotectedvars -> VS.t t
   | Invariant: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
   | MayAccessed: AccessDomain.EventSet.t t
-  | MayBeTainted: LS.t t
+  | MayBeTainted: AD.t t
   | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t
   | TmpSpecial:  Mval.Exp.t -> ML.t t
 
@@ -144,8 +146,8 @@ struct
     | MayPointTo _ -> (module AD)
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
-    | MustLockset -> (module LS)
-    | EvalFunvar _ -> (module LS)
+    | MustLockset -> (module AD)
+    | EvalFunvar _ -> (module AD)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
     | MayBePublic _ -> (module MayBool)
@@ -179,13 +181,13 @@ struct
     | CreatedThreads ->  (module ConcDomain.ThreadSet)
     | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
     | ThreadsJoinedCleanly -> (module MustBool)
-    | MustProtectedVars _ -> (module LS)
+    | MustProtectedVars _ -> (module VS)
     | Invariant _ -> (module Invariant)
     | InvariantGlobal _ -> (module Invariant)
     | WarnGlobal _ -> (module Unit)
     | IterSysVars _ -> (module Unit)
     | MayAccessed -> (module AccessDomain.EventSet)
-    | MayBeTainted -> (module LS)
+    | MayBeTainted -> (module AD)
     | MayBeModifiedSinceSetjmp _ -> (module VS)
     | TmpSpecial _ -> (module ML)
 
@@ -208,8 +210,8 @@ struct
     | MayPointTo _ -> AD.top ()
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
-    | MustLockset -> LS.top ()
-    | EvalFunvar _ -> LS.top ()
+    | MustLockset -> AD.top ()
+    | EvalFunvar _ -> AD.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
     | MayBePublic _ -> MayBool.top ()
@@ -243,13 +245,13 @@ struct
     | CreatedThreads -> ConcDomain.ThreadSet.top ()
     | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
     | ThreadsJoinedCleanly -> MustBool.top ()
-    | MustProtectedVars _ -> LS.top ()
+    | MustProtectedVars _ -> VS.top ()
     | Invariant _ -> Invariant.top ()
     | InvariantGlobal _ -> Invariant.top ()
     | WarnGlobal _ -> Unit.top ()
     | IterSysVars _ -> Unit.top ()
     | MayAccessed -> AccessDomain.EventSet.top ()
-    | MayBeTainted -> LS.top ()
+    | MayBeTainted -> AD.top ()
     | MayBeModifiedSinceSetjmp _ -> VS.top ()
     | TmpSpecial _ -> ML.top ()
 end
@@ -335,7 +337,12 @@ struct
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
       | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2
       | Any (EvalValue e1), Any (EvalValue e2) -> CilType.Exp.compare e1 e2
-      | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2
+      | Any (BlobSize {exp = e1; base_address = b1}), Any (BlobSize {exp = e2; base_address = b2}) ->
+        let r = CilType.Exp.compare e1 e2 in
+        if r <> 0 then
+          r
+        else
+          Stdlib.compare b1 b2
       | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2
       | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2
       | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2
@@ -380,7 +387,7 @@ struct
     | Any (EvalLength e) -> CilType.Exp.hash e
     | Any (EvalMutexAttr e) -> CilType.Exp.hash e
     | Any (EvalValue e) -> CilType.Exp.hash e
-    | Any (BlobSize e) -> CilType.Exp.hash e
+    | Any (BlobSize {exp = e; base_address = b}) -> CilType.Exp.hash e + Hashtbl.hash b
     | Any (CondVars e) -> CilType.Exp.hash e
     | Any (PartAccess p) -> hash_access p
     | Any (IterPrevVars i) -> 0
@@ -428,7 +435,7 @@ struct
     | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e
     | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e
     | Any (EvalValue e) -> Pretty.dprintf "EvalValue %a" CilType.Exp.pretty e
-    | Any (BlobSize e) -> Pretty.dprintf "BlobSize %a" CilType.Exp.pretty e
+    | Any (BlobSize {exp = e; base_address = b}) -> Pretty.dprintf "BlobSize %a (base_address: %b)" CilType.Exp.pretty e b
     | Any (CondVars e) -> Pretty.dprintf "CondVars %a" CilType.Exp.pretty e
     | Any (PartAccess p) -> Pretty.dprintf "PartAccess _"
     | Any (IterPrevVars i) -> Pretty.dprintf "IterPrevVars _"
diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml
index 0f3a9f55bc..32b4e4d608 100644
--- a/src/framework/analysisState.ml
+++ b/src/framework/analysisState.ml
@@ -7,6 +7,9 @@ let should_warn = ref false
 (** Whether signed overflow or underflow happened *)
 let svcomp_may_overflow = ref false
 
+(** Whether an invalid pointer dereference happened *)
+let svcomp_may_invalid_deref = ref false
+
 (** A hack to see if we are currently doing global inits *)
 let global_initialization = ref false
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 4efb0d5346..21f3958a81 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -302,7 +302,7 @@ struct
     | Queries.EvalFunvar e ->
       let (d,l) = ctx.local in
       if leq0 l then
-        Queries.LS.empty ()
+        Queries.AD.empty ()
       else
         query' ctx (Queries.EvalFunvar e)
     | q -> query' ctx q
@@ -754,8 +754,8 @@ struct
         [v]
       | _ ->
         (* Depends on base for query. *)
-        let ls = ctx.ask (Queries.EvalFunvar e) in
-        Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls []
+        let ad = ctx.ask (Queries.EvalFunvar e) in
+        Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
     let one_function f =
       match f.vtype with
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 625e81f18b..6e700485dd 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -85,6 +85,7 @@ module MallocFresh = MallocFresh
 module Malloc_null = Malloc_null
 module MemLeak = MemLeak
 module UseAfterFree = UseAfterFree
+module MemOutOfBounds = MemOutOfBounds
 
 (** {2 Concurrency}
 
diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index d1c8f0db3c..1bb31d6d5b 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -11,6 +11,7 @@ type undefined_behavior =
   | ArrayOutOfBounds of array_oob
   | NullPointerDereference
   | UseAfterFree
+  | MemoryOutOfBoundsAccess
   | DoubleFree
   | InvalidMemoryDeallocation
   | MemoryLeak
@@ -66,6 +67,7 @@ struct
     let array_out_of_bounds e: category = create @@ ArrayOutOfBounds e
     let nullpointer_dereference: category = create @@ NullPointerDereference
     let use_after_free: category = create @@ UseAfterFree
+    let memory_out_of_bounds_access: category = create @@ MemoryOutOfBoundsAccess
     let double_free: category = create @@ DoubleFree
     let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation
     let memory_leak: category = create @@ MemoryLeak
@@ -105,6 +107,7 @@ struct
         | "array_out_of_bounds" -> ArrayOutOfBounds.from_string_list t
         | "nullpointer_dereference" -> nullpointer_dereference
         | "use_after_free" -> use_after_free
+        | "memory_out_of_bounds_access" -> memory_out_of_bounds_access
         | "double_free" -> double_free
         | "invalid_memory_deallocation" -> invalid_memory_deallocation
         | "uninitialized" -> uninitialized
@@ -117,6 +120,7 @@ struct
       | ArrayOutOfBounds e -> "ArrayOutOfBounds" :: ArrayOutOfBounds.path_show e
       | NullPointerDereference -> ["NullPointerDereference"]
       | UseAfterFree -> ["UseAfterFree"]
+      | MemoryOutOfBoundsAccess -> ["MemoryOutOfBoundsAccess"]
       | DoubleFree -> ["DoubleFree"]
       | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"]
       | MemoryLeak -> ["MemoryLeak"]
@@ -229,6 +233,7 @@ let behaviorName = function
   |Undefined u -> match u with
     |NullPointerDereference -> "NullPointerDereference"
     |UseAfterFree -> "UseAfterFree"
+    |MemoryOutOfBoundsAccess -> "MemoryOutOfBoundsAccess"
     |DoubleFree -> "DoubleFree"
     |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation"
     |MemoryLeak -> "MemoryLeak"
diff --git a/tests/regression/01-cpa/33-asserts.c b/tests/regression/01-cpa/33-asserts.c
index f8bf6c3132..26efad44fc 100644
--- a/tests/regression/01-cpa/33-asserts.c
+++ b/tests/regression/01-cpa/33-asserts.c
@@ -26,14 +26,14 @@ int main(){
   check(j==6); // assert UNKNOWN
 
   unknown(&k);
-  assume(k==4); // TODO? assert SUCCESS
+  assume(k==4);
   check(k==4);  // assert SUCCESS
 
   unknown(&k);
-  assume(k+1==n); // TODO? FAIL
+  assume(k+1==n);
 
-  assume(n==5);  // TODO? NOWARN
-  assert(0);     // NOWARN
+  assume(n==5);  // contradiction
+  assert(0);     // NOWARN (unreachable)
 
   return 0;
 }
\ No newline at end of file
diff --git a/tests/regression/04-mutex/58-pthread-lock-return.c b/tests/regression/04-mutex/58-pthread-lock-return.c
new file mode 100644
index 0000000000..3e2a05c94e
--- /dev/null
+++ b/tests/regression/04-mutex/58-pthread-lock-return.c
@@ -0,0 +1,118 @@
+// PARAM: --disable sem.lock.fail
+#include <pthread.h>
+
+int g_mutex = 0;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+int g_rwlock = 0;
+pthread_rwlock_t rwlock = PTHREAD_RWLOCK_INITIALIZER;
+
+// OS X has no spinlock
+#ifndef __APPLE__
+int g_spin = 0;
+pthread_spinlock_t spin;
+#endif
+
+void *t_fun(void *arg) {
+  if (!pthread_mutex_lock(&mutex)) {
+    __goblint_check(1); // reachable
+    g_mutex++; // NORACE
+    pthread_mutex_unlock(&mutex);
+  }
+  else {
+    __goblint_check(0); // NOWARN (unreachable)
+  }
+
+  if (!pthread_mutex_trylock(&mutex)) {
+    __goblint_check(1); // reachable
+    g_mutex++; // NORACE
+    pthread_mutex_unlock(&mutex);
+  }
+  else {
+    __goblint_check(1); // reachable
+  }
+
+  if (!pthread_rwlock_wrlock(&mutex)) {
+    __goblint_check(1); // reachable
+    g_rwlock++; // NORACE
+    pthread_rwlock_unlock(&mutex);
+  }
+  else {
+    __goblint_check(0); // NOWARN (unreachable)
+  }
+
+  if (!pthread_rwlock_trywrlock(&mutex)) {
+    __goblint_check(1); // reachable
+    g_rwlock++; // NORACE
+    pthread_rwlock_unlock(&mutex);
+  }
+  else {
+    __goblint_check(1); // reachable
+  }
+
+  if (!pthread_rwlock_rdlock(&mutex)) {
+    __goblint_check(1); // reachable
+    g_rwlock++; // NORACE
+    pthread_rwlock_unlock(&mutex);
+  }
+  else {
+    __goblint_check(0); // NOWARN (unreachable)
+  }
+
+  if (!pthread_rwlock_tryrdlock(&mutex)) {
+    __goblint_check(1); // reachable
+    g_rwlock++; // NORACE
+    pthread_rwlock_unlock(&mutex);
+  }
+  else {
+    __goblint_check(1); // reachable
+  }
+
+#ifndef __APPLE__
+  if (!pthread_spin_lock(&spin)) {
+    __goblint_check(1); // TODO reachable (TODO for OSX)
+    g_spin++; // NORACE
+    pthread_spin_unlock(&spin);
+  }
+  else {
+    __goblint_check(0); // NOWARN (unreachable)
+  }
+
+  if (!pthread_spin_trylock(&spin)) {
+    __goblint_check(1); // TODO reachable (TODO for OSX)
+    g_spin++; // NORACE
+    pthread_spin_unlock(&spin);
+  }
+  else {
+    __goblint_check(1); // TODO reachable (TODO for OSX)
+  }
+#endif
+
+  return NULL;
+}
+
+int main() {
+#ifndef __APPLE__
+  pthread_spin_init(&spin, PTHREAD_PROCESS_PRIVATE);
+#endif
+
+  pthread_t id;
+  pthread_create(&id, NULL, &t_fun, NULL);
+
+  pthread_mutex_lock(&mutex);
+  g_mutex++; // NORACE
+  pthread_mutex_unlock(&mutex);
+
+  pthread_rwlock_wrlock(&mutex);
+  g_rwlock++; // NORACE
+  pthread_rwlock_unlock(&mutex);
+
+#ifndef __APPLE__
+  pthread_spin_lock(&spin);
+  g_spin++; // NORACE
+  pthread_spin_unlock(&spin);
+#endif
+
+  pthread_join(id, NULL);
+  return 0;
+}
diff --git a/tests/regression/05-lval_ls/20-race-null-void.c b/tests/regression/05-lval_ls/20-race-null-void.c
new file mode 100644
index 0000000000..1950ada73e
--- /dev/null
+++ b/tests/regression/05-lval_ls/20-race-null-void.c
@@ -0,0 +1,54 @@
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void **top;
+  free(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      pthread_join(id, NULL); // NORACE
+      break;
+    case 1:
+      pthread_join(id, 0); // NORACE
+      break;
+    case 2:
+      pthread_join(id, zero); // NORACE
+      break;
+    case 3:
+      pthread_join(id, 1); // RACE
+      break;
+    case 4:
+      pthread_join(id, one); // RACE
+      break;
+    case 5:
+      pthread_join(id, r); // RACE
+      break;
+    case 6:
+      pthread_join(id, null); // NORACE
+      break;
+    case 7:
+      pthread_join(id, unknown); // RACE
+      break;
+    case 8:
+      pthread_join(id, top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}
diff --git a/tests/regression/05-lval_ls/21-race-null-type.c b/tests/regression/05-lval_ls/21-race-null-type.c
new file mode 100644
index 0000000000..6b5e6e42fd
--- /dev/null
+++ b/tests/regression/05-lval_ls/21-race-null-type.c
@@ -0,0 +1,55 @@
+// PARAM: --enable ana.race.direct-arithmetic
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void *top;
+  time(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      time(NULL); // NORACE
+      break;
+    case 1:
+      time(0); // NORACE
+      break;
+    case 2:
+      time(zero); // NORACE
+      break;
+    case 3:
+      time(1); // RACE
+      break;
+    case 4:
+      time(one); // RACE
+      break;
+    case 5:
+      time(r); // RACE
+      break;
+    case 6:
+      time(null); // NORACE
+      break;
+    case 7:
+      time(unknown); // RACE
+      break;
+    case 8:
+      time(top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}
diff --git a/tests/regression/05-lval_ls/22-race-null-void-deep.c b/tests/regression/05-lval_ls/22-race-null-void-deep.c
new file mode 100644
index 0000000000..7e99f286b6
--- /dev/null
+++ b/tests/regression/05-lval_ls/22-race-null-void-deep.c
@@ -0,0 +1,56 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_key_t key;
+
+void *t_fun(void *arg) {
+  void *top;
+  pthread_setspecific(key, top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      pthread_setspecific(key, NULL); // NORACE
+      break;
+    case 1:
+      pthread_setspecific(key, 0); // NORACE
+      break;
+    case 2:
+      pthread_setspecific(key, zero); // NORACE
+      break;
+    case 3:
+      pthread_setspecific(key, 1); // RACE
+      break;
+    case 4:
+      pthread_setspecific(key, one); // RACE
+      break;
+    case 5:
+      pthread_setspecific(key, r); // RACE
+      break;
+    case 6:
+      pthread_setspecific(key, null); // NORACE
+      break;
+    case 7:
+      pthread_setspecific(key, unknown); // RACE
+      break;
+    case 8:
+      pthread_setspecific(key, top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}
diff --git a/tests/regression/05-lval_ls/23-race-null-type-deep.c b/tests/regression/05-lval_ls/23-race-null-type-deep.c
new file mode 100644
index 0000000000..6f29964d1e
--- /dev/null
+++ b/tests/regression/05-lval_ls/23-race-null-type-deep.c
@@ -0,0 +1,54 @@
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void *top;
+  fclose(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      feof(NULL); // NORACE
+      break;
+    case 1:
+      feof(0); // NORACE
+      break;
+    case 2:
+      feof(zero); // NORACE
+      break;
+    case 3:
+      feof(1); // RACE
+      break;
+    case 4:
+      feof(one); // RACE
+      break;
+    case 5:
+      feof(r); // RACE
+      break;
+    case 6:
+      feof(null); // NORACE
+      break;
+    case 7:
+      feof(unknown); // RACE
+      break;
+    case 8:
+      feof(top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}
diff --git a/tests/regression/28-race_reach/22-deref_read_racefree.c b/tests/regression/28-race_reach/22-deref_read_racefree.c
index 3386277083..2e4c5ebbb6 100644
--- a/tests/regression/28-race_reach/22-deref_read_racefree.c
+++ b/tests/regression/28-race_reach/22-deref_read_racefree.c
@@ -17,7 +17,7 @@ int main() {
   create_threads(t);
   q = p;
   pthread_mutex_lock(&mutex);
-  assert_racefree(*q);  // TODO
+  assert_racefree(*q);
   pthread_mutex_unlock(&mutex);
   return 0;
 }
diff --git a/tests/regression/28-race_reach/61-invariant_racing.c b/tests/regression/28-race_reach/61-invariant_racing.c
index 3facd56d32..22277557f9 100644
--- a/tests/regression/28-race_reach/61-invariant_racing.c
+++ b/tests/regression/28-race_reach/61-invariant_racing.c
@@ -6,9 +6,12 @@ pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
-  if (x == 0) {
+  pthread_mutex_lock(&__global_lock);
+  if (x == 0) { // NORACE
+    pthread_mutex_unlock(&__global_lock);
     pthread_mutex_unlock(&mutex);
   } else {
+    pthread_mutex_unlock(&__global_lock);
     pthread_mutex_unlock(&mutex);
     access(x);
   }
diff --git a/tests/regression/41-stdlib/07-atexit.c b/tests/regression/41-stdlib/07-atexit.c
new file mode 100644
index 0000000000..4551400175
--- /dev/null
+++ b/tests/regression/41-stdlib/07-atexit.c
@@ -0,0 +1,13 @@
+#include <stdlib.h>
+#include <goblint.h>
+
+void bye()
+{
+  __goblint_check(1); // reachable
+}
+
+int main()
+{
+  atexit(bye);
+  return 0;
+}
diff --git a/tests/regression/41-stdlib/08-atexit-no-spawn.c b/tests/regression/41-stdlib/08-atexit-no-spawn.c
new file mode 100644
index 0000000000..7f25f42183
--- /dev/null
+++ b/tests/regression/41-stdlib/08-atexit-no-spawn.c
@@ -0,0 +1,14 @@
+// PARAM: --disable sem.unknown_function.spawn
+#include <stdlib.h>
+#include <goblint.h>
+
+void bye()
+{
+  __goblint_check(0); // NOWARN (unreachable)
+}
+
+int main()
+{
+  atexit(bye);
+  return 0;
+}
diff --git a/tests/regression/66-interval-set-one/51-widen-sides.c b/tests/regression/66-interval-set-one/51-widen-sides.c
index 72eb1396b1..b086baf026 100644
--- a/tests/regression/66-interval-set-one/51-widen-sides.c
+++ b/tests/regression/66-interval-set-one/51-widen-sides.c
@@ -3,13 +3,13 @@
 
 int further(int n) {
     // Even sides-local can not save us here :(
-    __goblint_check(n <= 1); //TODO
+    __goblint_check(n <= 2); //TODO
 }
 
 
 int fun(int n, const char* arg) {
     // Fails with solvers.td3.side_widen sides, needs sides-local
-    __goblint_check(n <= 1);
+    __goblint_check(n <= 2);
     further(n);
 }
 
@@ -26,5 +26,5 @@ int main() {
     doIt("two");
 
     // In the setting with solvers.td3.side_widen sides, widening happens and the bound is lost
-    fun(1, "org");
+    fun(2, "org");
 }
diff --git a/tests/regression/77-mem-oob/01-oob-heap-simple.c b/tests/regression/77-mem-oob/01-oob-heap-simple.c
new file mode 100644
index 0000000000..10c7864184
--- /dev/null
+++ b/tests/regression/77-mem-oob/01-oob-heap-simple.c
@@ -0,0 +1,14 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(5 * sizeof(char));
+
+    *ptr = 'a';//NOWARN
+    *(ptr + 1) = 'b';//NOWARN
+    *(ptr + 10) = 'c';//WARN
+
+    free(ptr);
+
+    return 0;
+}
diff --git a/tests/regression/77-mem-oob/02-oob-stack-simple.c b/tests/regression/77-mem-oob/02-oob-stack-simple.c
new file mode 100644
index 0000000000..8d022feca4
--- /dev/null
+++ b/tests/regression/77-mem-oob/02-oob-stack-simple.c
@@ -0,0 +1,12 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+
+int main(int argc, char const *argv[]) {
+    int i = 42;
+    int *ptr = &i;
+
+    *ptr = 5;//NOWARN
+    *(ptr + 10) = 55;//WARN
+
+    return 0;
+}
diff --git a/tests/regression/77-mem-oob/03-oob-loop.c b/tests/regression/77-mem-oob/03-oob-loop.c
new file mode 100644
index 0000000000..4f637d487e
--- /dev/null
+++ b/tests/regression/77-mem-oob/03-oob-loop.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --set exp.unrolling-factor 10 --enable ana.int.interval
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(5 * sizeof(char));
+    
+    for (int i = 0; i < 10; i++) {
+        ptr++;
+    }
+
+    printf("%s", *ptr); //WARN
+    free(ptr); //WARN
+
+    return 0;
+}
diff --git a/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c b/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c
new file mode 100644
index 0000000000..5046a00664
--- /dev/null
+++ b/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c
@@ -0,0 +1,18 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+#include <stdio.h>
+
+int main(int argc, char const *argv[]) {
+    char *ptr = malloc(5 * sizeof(char));
+
+    ptr++;//NOWARN
+    printf("%s", *ptr);//NOWARN
+    ptr = ptr + 5;//NOWARN
+    printf("%s", *ptr);//WARN
+    *(ptr + 1) = 'b';//WARN
+    *(ptr + 10) = 'c';//WARN
+
+    free(ptr);
+
+    return 0;
+}
diff --git a/tests/regression/77-mem-oob/05-oob-implicit-deref.c b/tests/regression/77-mem-oob/05-oob-implicit-deref.c
new file mode 100644
index 0000000000..8bec6a72e0
--- /dev/null
+++ b/tests/regression/77-mem-oob/05-oob-implicit-deref.c
@@ -0,0 +1,23 @@
+// 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>
+
+int main(int argc, char const *argv[]) {
+    int *ptr = malloc(4 * sizeof(int));
+
+    // Both lines below are considered derefs => no need to warn, since ptr is pointing within its bounds
+    memset(ptr, 0, 4 * sizeof(int)); //NOWARN
+    printf("%p", (void *) ptr); //NOWARN
+    ptr = ptr + 10; // ptr no longer points within its allocated bounds
+
+    // Each of both lines below should now receive a WARN
+    memset(ptr, 0, 4 * sizeof(int)); //WARN
+    printf("%p", (void *) ptr); //WARN
+
+    return 0;
+}