diff --git a/dune-project b/dune-project
index 2fbfb271fc..b8b8481c97 100644
--- a/dune-project
+++ b/dune-project
@@ -44,7 +44,7 @@
     (fileutils (>= 0.6.4))
     cpu
     arg-complete
-    yaml
+    (yaml (>= 3.0.0))
     uuidm
     catapult
     catapult-file
diff --git a/goblint.opam b/goblint.opam
index 678ad53d13..a20df919d0 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -41,7 +41,7 @@ depends: [
   "fileutils" {>= "0.6.4"}
   "cpu"
   "arg-complete"
-  "yaml"
+  "yaml" {>= "3.0.0"}
   "uuidm"
   "catapult"
   "catapult-file"
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index e63d47ab5c..71e2661997 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2289,15 +2289,17 @@ struct
           let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
           if ID.to_int countval = Some Z.one then (
             set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
-              add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false);
-              eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))
+              (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
+              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))
             ]
           )
           else (
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
             (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
-                                                          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+              (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
+              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))
+            ]
           )
         | _ -> st
       end
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index bf7035b9d4..6003f69bf9 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -196,6 +196,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("unsetenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]);
     ("lseek", unknown [drop "fd" []; drop "offset" []; drop "whence" []]);
     ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w])));
+    ("__open_missing_mode", unknown []);
     ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]);
     ("fileno", unknown [drop "stream" [r_deep; w_deep]]);
     ("fdopen", unknown [drop "fd" []; drop "mode" [r]]);
@@ -287,6 +288,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []]); (* TODO: use Call instead of Spawn *)
     ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
     ("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" []]);
   ]
 
 (** Pthread functions. *)
@@ -352,6 +354,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
     ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
     ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *)
+    ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
+    ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]);
   ]
 
 (** GCC builtin functions.
@@ -462,6 +466,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("sysinfo", unknown [drop "info" [w_deep]]);
     ("__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" []]);
   ]
 
 let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
@@ -811,6 +816,15 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wbkgd", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
   ]
 
+let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("pcre_compile", unknown [drop "pattern" [r]; drop "options" []; drop "errptr" [w]; drop "erroffset" [w]; drop "tableptr" [r]]);
+    ("pcre_compile2", unknown [drop "pattern" [r]; drop "options" []; drop "errorcodeptr" [w]; drop "errptr" [w]; drop "erroffset" [w]; drop "tableptr" [r]]);
+    ("pcre_config", unknown [drop "what" []; drop "where" [w]]);
+    ("pcre_exec", unknown [drop "code" [r_deep]; drop "extra" [r_deep]; drop "subject" [r]; drop "length" []; drop "startoffset" []; drop "options" []; drop "ovector" [w]; drop "ovecsize" []]);
+    ("pcre_study", unknown [drop "code" [r_deep]; drop "options" []; drop "errptr" [w]]);
+    ("pcre_version", unknown []);
+  ]
+
 let libraries = Hashtbl.of_list [
     ("c", c_descs_list @ math_descs_list);
     ("posix", posix_descs_list);
@@ -823,6 +837,7 @@ let libraries = Hashtbl.of_list [
     ("sv-comp", svcomp_descs_list);
     ("ncurses", ncurses_descs_list);
     ("zstd", zstd_descs_list);
+    ("pcre", pcre_descs_list);
   ]
 
 let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index f3301a4659..fabd655811 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -3,6 +3,128 @@
 open GoblintCil
 open Analyses
 
+(** Data race analysis with tries for offsets and type-based memory locations for open code.
+
+    Accesses are to memory locations ({{!Access.Memo} memos}) which consist of a root and offset.
+    {{!Access.MemoRoot} Root} can be:
+    + variable, if access is to known global variable or alloc-variable;
+    + type, if access is to unknown pointer.
+
+    Accesses are (now) collected to sets for each corresponding memo,
+    after points-to sets are resolved, during postsolving.
+
+    Race checking is performed per-memo,
+    except must additionally account for accesses to other memos (see diagram below):
+    + access to [s.f] can race with access to a prefix like [s], which writes an entire struct at once;
+    + access to [s.f] can race with type-based access like [(struct S).f];
+    + access to [(struct S).f] can race with type-based access to a suffix like [(int)].
+    + access to [(struct T).s.f] can race with type-based access like [(struct S)], which is a combination of the above.
+
+    These are accounted for lazily (unlike in the past).
+
+    Prefixes (a.k.a. inner distribution) are handled using a trie data structure enriched with lattice properties.
+    Race checking starts at the root and passes accesses to ancestor nodes down to children.
+
+    Type suffixes (a.k.a. outer distribution) are handled by computing successive immediate type suffixes transitively
+    and accessing corresponding offsets from corresponding root tries in the global invariant.
+
+    Type suffix prefixes (for the combination of the two) are handled by passing type suffix accesses down when traversing the prefix trie.
+
+    Race checking happens at each trie node with the above three access sets at hand using {!Access.group_may_race}.
+    All necessary combinations between the four classes are handled, but unnecessary repeated work is carefully avoided.
+    E.g. accesses which are pairwise checked at some prefix are not re-checked pairwise at a node.
+    Thus, races (with prefixes or type suffixes) are reported for most precise memos with actual accesses:
+    at the longest prefix and longest type suffix.
+
+    Additionally, accesses between prefix and type suffix intersecting at a node are checked.
+    These races are reported at the unique memo at the intersection of the prefix and the type suffix.
+    This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets.
+    It ensures that corresponding trie nodes exist for traversal later. *)
+
+(** Given C declarations:
+    {@c[
+    struct S {
+      int f;
+    };
+
+    struct T {
+      struct S s;
+    };
+
+    struct T t;
+    ]}
+
+    Example structure of related memos for race checking:
+    {v
+     (int)   (S)     (T)
+        \   /   \   /   \
+          f       s       t
+            \   /   \   /
+              f       s
+                \   /
+                  f
+    v}
+    where:
+    - [(int)] is a type-based memo root for the primitive [int] type;
+    - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots;
+    - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left;
+    - type suffix relations are indicated by [\ ].
+
+    All same-node races:
+    - Race between [t.s.f] and [t.s.f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [t.s] is checked/reported at [t.s].
+    - Race between [t] and [t] is checked/reported at [t].
+    - Race between [(T).s.f] and [(T).s.f] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(T).s] is checked/reported at [(T).s].
+    - Race between [(T)] and [(T)] is checked/reported at [(T)].
+    - Race between [(S).f] and [(S).f] is checked/reported at [(S).f].
+    - Race between [(S)] and [(S)] is checked/reported at [(S)].
+    - Race between [(int)] and [(int)] is checked/reported at [(int)].
+
+    All prefix races:
+    - Race between [t.s.f] and [t.s] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [t] is checked/reported at [t.s.f].
+    - Race between [t.s] and [t] is checked/reported at [t.s].
+    - Race between [(T).s.f] and [(T).s] is checked/reported at [(T).s.f].
+    - Race between [(T).s.f] and [(T)] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(T)] is checked/reported at [(T).s].
+    - Race between [(S).f] and [(S)] is checked/reported at [(S).f].
+
+    All type suffix races:
+    - Race between [t.s.f] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(int)] is checked/reported at [t.s.f].
+    - Race between [(T).s.f] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T).s.f] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(S).f] and [(int)] is checked/reported at [(S).f].
+    - Race between [t.s] and [(T).s] is checked/reported at [t.s].
+    - Race between [t.s] and [(S)] is checked/reported at [t.s].
+    - Race between [(T).s] and [(S)] is checked/reported at [(T).s].
+    - Race between [t] and [(T)] is checked/reported at [t].
+
+    All type suffix prefix races:
+    - Race between [t.s.f] and [(T).s] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(T)] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(S)] is checked/reported at [t.s.f].
+    - Race between [(T).s.f] and [(S)] is checked/reported at [(T).s.f].
+    - Race between [t.s] and [(T)] is checked/reported at [t.s].
+
+    All prefix-type suffix races:
+    - Race between [t.s] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [(int)] is checked/reported at [t.s.f].
+    - Race between [t] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t] and [(int)] is checked/reported at [t.s.f].
+    - Race between [t] and [(T).s] is checked/reported at [t.s].
+    - Race between [t] and [(S)] is checked/reported at [t.s].
+    - Race between [(T).s] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(S)] is checked/reported at [(T).s].
+    - Race between [(S)] and [(int)] is checked/reported at [(S).f]. *)
+
 
 (** Data race analyzer without base --- this is the new standard *)
 module Spec =
@@ -12,7 +134,7 @@ struct
   let name () = "race"
 
   (* Two global invariants:
-     1. memoroot -> (offset -> accesses)  --  used for warnings
+     1. memoroot -> (offset --trie--> accesses)  --  used for warnings
      2. varinfo -> set of memo  --  used for IterSysVars Global *)
 
   module V =
@@ -52,13 +174,22 @@ struct
 
   module OffsetTrie =
   struct
-    include TrieDomain.Make (OneOffset) (Access.AS)
+    (* LiftBot such that add_distribute_outer can side-effect empty set to indicate
+       all offsets that exist for prefix-type_suffix race checking.
+       Otherwise, there are no trie nodes to traverse to where this check must happen. *)
+    include TrieDomain.Make (OneOffset) (Lattice.LiftBot (Access.AS))
+
+    let rec find (offset : Offset.Unit.t) ((accs, children) : t) : value =
+      match offset with
+      | `NoOffset -> accs
+      | `Field (f, offset') -> find offset' (ChildMap.find (Field f) children)
+      | `Index ((), offset') -> find offset' (ChildMap.find Index children)
 
     let rec singleton (offset : Offset.Unit.t) (value : value) : t =
       match offset with
       | `NoOffset -> (value, ChildMap.empty ())
-      | `Field (f, offset') -> (Access.AS.empty (), ChildMap.singleton (Field f) (singleton offset' value))
-      | `Index ((), offset') -> (Access.AS.empty (), ChildMap.singleton Index (singleton offset' value))
+      | `Field (f, offset') -> (`Bot, ChildMap.singleton (Field f) (singleton offset' value))
+      | `Index ((), offset') -> (`Bot, ChildMap.singleton Index (singleton offset' value))
   end
 
   module G =
@@ -96,9 +227,42 @@ struct
 
   let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (Access.AS.singleton (conf, w, loc, e, a))));
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a)))));
+    side_vars ctx memo
+
+  (** Side-effect empty access set for prefix-type_suffix race checking. *)
+  let side_access_empty ctx ((memoroot, offset) as memo) =
+    if !AnalysisState.should_warn then
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.empty ()))));
     side_vars ctx memo
 
+  (** Get immediate type_suffix memo. *)
+  let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option =
+    (* No need to make ana.race.direct-arithmetic return None here,
+       because (int) is empty anyway since Access.add_distribute_outer isn't called. *)
+    match root, offset with
+    | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *)
+    | _, `NoOffset -> None (* primitive type *)
+    | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *)
+    | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *)
+    | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)
+
+  let rec find_type_suffix' ctx ((root, offset) as memo : Access.Memo.t) : Access.AS.t =
+    let trie = G.access (ctx.global (V.access root)) in
+    let accs =
+      match OffsetTrie.find offset trie with
+      | `Lifted accs -> accs
+      | `Bot -> Access.AS.empty ()
+    in
+    let type_suffix = find_type_suffix ctx memo in
+    Access.AS.union accs type_suffix
+
+  (** Find accesses from all type_suffixes transitively. *)
+  and find_type_suffix ctx (memo : Access.Memo.t) : Access.AS.t =
+    match type_suffix_memo memo with
+    | Some type_suffix_memo -> find_type_suffix' ctx type_suffix_memo
+    | None -> Access.AS.empty ()
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | WarnGlobal g ->
@@ -108,18 +272,27 @@ struct
           (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *)
           let trie = G.access (ctx.global g) in
           (** Distribute access to contained fields. *)
-          let rec distribute_inner offset (accs, children) ancestor_accs =
-            let ancestor_accs' = Access.AS.union ancestor_accs accs in
-            OffsetTrie.ChildMap.iter (fun child_key child_trie ->
-                distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ancestor_accs'
-              ) children;
-            if not (Access.AS.is_empty accs) then (
+          let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix =
+            let accs =
+              match accs with
+              | `Lifted accs -> accs
+              | `Bot -> Access.AS.empty ()
+            in
+            let type_suffix = find_type_suffix ctx (g', offset) in
+            if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then (
               let memo = (g', offset) in
               let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in
-              Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo) accs
-            )
+              Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {node=accs; prefix; type_suffix; type_suffix_prefix}) memo
+            );
+
+            (* Recurse to children. *)
+            let prefix' = Access.AS.union prefix accs in
+            let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in
+            OffsetTrie.ChildMap.iter (fun child_key child_trie ->
+                distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~prefix:prefix' ~type_suffix_prefix:type_suffix_prefix'
+              ) children;
           in
-          distribute_inner `NoOffset trie (Access.AS.empty ())
+          distribute_inner `NoOffset trie ~prefix:(Access.AS.empty ()) ~type_suffix_prefix:(Access.AS.empty ())
         | `Right _ -> (* vars *)
           ()
       end
@@ -142,11 +315,11 @@ struct
       let loc = Option.get !Node.current_node in
       let add_access conf voffs =
         let a = part_access (Option.map fst voffs) in
-        Access.add (side_access octx (conf, kind, loc, e, a)) e voffs;
+        Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs;
       in
       let add_access_struct conf ci =
         let a = part_access None in
-        Access.add_one (side_access octx (conf, kind, loc, e, a)) (`Type (TComp (ci, [])), `NoOffset)
+        Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
       in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls
diff --git a/src/domains/access.ml b/src/domains/access.ml
index a183a32633..675d1c2e72 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -84,8 +84,7 @@ type acc_typ = [ `Type of CilType.Typ.t | `Struct of CilType.Compinfo.t * Offset
 module MemoRoot =
 struct
   include Printable.StdLeaf
-  type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typ.t] [@@deriving eq, ord, hash]
-  (* Can't use typsig for `Type because there's no function to follow offsets on typsig. *)
+  type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typsig.t] [@@deriving eq, ord, hash]
 
   let name () = "memoroot"
 
@@ -93,8 +92,8 @@ struct
     (* Imitate old printing for now *)
     match vt with
     | `Var v -> CilType.Varinfo.pretty () v
-    | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)" c.cname
-    | `Type t -> Pretty.dprintf "(%a)" CilType.Typ.pretty t
+    | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)" name
+    | `Type t -> Pretty.dprintf "(%a)" Cilfacade.pretty_typsig_like_typ t
 
   include Printable.SimplePretty (
     struct
@@ -109,7 +108,6 @@ module Memo =
 struct
   include Printable.StdLeaf
   type t = MemoRoot.t * Offset.Unit.t [@@deriving eq, ord, hash]
-  (* Can't use typsig for `Type because there's no function to follow offsets on typsig. *)
 
   let name () = "memo"
 
@@ -117,8 +115,8 @@ struct
     (* Imitate old printing for now *)
     match vt with
     | `Var v -> Pretty.dprintf "%a%a" CilType.Varinfo.pretty v Offset.Unit.pretty o
-    | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)%a" c.cname Offset.Unit.pretty o
-    | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typ.pretty t Offset.Unit.pretty o
+    | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)%a" name Offset.Unit.pretty o
+    | `Type t -> Pretty.dprintf "(%a)%a" Cilfacade.pretty_typsig_like_typ t Offset.Unit.pretty o
 
   include Printable.SimplePretty (
     struct
@@ -129,23 +127,14 @@ struct
 
   let of_ty (ty: acc_typ): t =
     match ty with
-    | `Struct (c, o) -> (`Type (TComp (c, [])), o)
-    | `Type t -> (`Type t, `NoOffset)
+    | `Struct (c, o) -> (`Type (TSComp (c.cstruct, c.cname, [])), o)
+    | `Type t -> (`Type (Cil.typeSig t), `NoOffset)
 
   let to_mval: t -> Mval.Unit.t option = function
     | (`Var v, o) -> Some (v, o)
     | (`Type _, _) -> None
 
   let add_offset ((vt, o): t) o2: t = (vt, Offset.Unit.add_offset o o2)
-
-  let type_of_base ((vt, _): t): typ =
-    match vt with
-    | `Var v -> v.vtype
-    | `Type t -> t
-
-  (** @raise Offset.Type_of_error *)
-  let type_of ((vt, o) as memo: t): typ =
-    Offset.Unit.type_of ~base:(type_of_base memo) o
 end
 
 (* TODO: What is the logic for get_type? *)
@@ -205,42 +194,43 @@ let get_val_type e: acc_typ =
 
 
 (** Add access to {!Memo} after distributing. *)
-let add_one side memo: unit =
+let add_one ~side memo: unit =
   let mv = Memo.to_mval memo in
   let ignorable = is_ignorable mv in
   if M.tracing then M.trace "access" "add_one %a (ignorable = %B)\n" Memo.pretty memo ignorable;
   if not ignorable then
     side memo
 
-(** Distribute type-based access to variables and containing fields. *)
-let rec add_distribute_outer side (t: typ) (o: Offset.Unit.t) =
-  let memo = (`Type t, o) in
+(** Distribute empty access set for type-based access to variables and containing fields.
+    Empty access sets are needed for prefix-type_suffix race checking. *)
+let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) =
+  let memo = (`Type ts, o) in
   if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo;
-  add_one side memo;
+  add_one ~side memo; (* Add actual access for non-recursive call, or empty access for recursive call when side is side_empty. *)
 
   (* distribute to variables of the type *)
-  let ts = typeSig t in
   let vars = TSH.find_all typeVar ts in
   List.iter (fun v ->
-      add_one side (`Var v, o) (* same offset, but on variable *)
+      (* same offset, but on variable *)
+      add_one ~side:side_empty (`Var v, o) (* Switch to side_empty. *)
     ) vars;
 
   (* recursively distribute to fields containing the type *)
   let fields = TSH.find_all typeIncl ts in
   List.iter (fun f ->
       (* prepend field and distribute to outer struct *)
-      add_distribute_outer side (TComp (f.fcomp, [])) (`Field (f, o))
+      add_distribute_outer ~side:side_empty ~side_empty (TSComp (f.fcomp.cstruct, f.fcomp.cname, [])) (`Field (f, o)) (* Switch to side_empty. *)
     ) fields;
 
   if M.tracing then M.traceu "access" "add_distribute_outer\n"
 
 (** Add access to known variable with offsets or unknown variable from expression. *)
-let add side e voffs =
+let add ~side ~side_empty e voffs =
   begin match voffs with
     | Some (v, o) -> (* known variable *)
       if M.tracing then M.traceli "access" "add var %a%a\n" CilType.Varinfo.pretty v CilType.Offset.pretty o;
       let memo = (`Var v, Offset.Unit.of_cil o) in
-      add_one side memo
+      add_one ~side memo
     | None -> (* unknown variable *)
       if M.tracing then M.traceli "access" "add type %a\n" CilType.Exp.pretty e;
       let ty = get_val_type e in (* extract old acc_typ from expression *)
@@ -250,7 +240,7 @@ let add side e voffs =
       in
       match o with
       | `NoOffset when not !collect_direct_arithmetic && isArithmeticType t -> ()
-      | _ -> add_distribute_outer side t o (* distribute to variables and outer offsets *)
+      | _ -> add_distribute_outer ~side ~side_empty (Cil.typeSig t) o (* distribute to variables and outer offsets *)
   end;
   if M.tracing then M.traceu "access" "add\n"
 
@@ -379,10 +369,48 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo
   else
     true
 
-let group_may_race ~ancestor_accs accs =
+(** Access sets for race detection and warnings. *)
+module WarnAccs =
+struct
+  type t = {
+    node: AS.t; (** Accesses for current memo. From accesses at trie node corresponding to memo offset. *)
+    prefix: AS.t; (** Accesses for all prefixes. From accesses to trie node ancestors. *)
+    type_suffix: AS.t; (** Accesses for all type suffixes. From offset suffixes in other tries. *)
+    type_suffix_prefix: AS.t; (** Accesses to all prefixes of all type suffixes. *)
+  }
+
+  let diff w1 w2 = {
+    node = AS.diff w1.node w2.node;
+    prefix = AS.diff w1.prefix w2.prefix;
+    type_suffix = AS.diff w1.type_suffix w2.type_suffix;
+    type_suffix_prefix = AS.diff w1.type_suffix_prefix w2.type_suffix_prefix;
+  }
+
+  let union_all w =
+    AS.union
+      (AS.union w.node w.prefix)
+      (AS.union w.type_suffix w.type_suffix_prefix)
+
+  let is_empty w =
+    AS.is_empty w.node && AS.is_empty w.prefix && AS.is_empty w.type_suffix && AS.is_empty w.type_suffix_prefix
+
+  let empty () =
+    {node=AS.empty (); prefix=AS.empty (); type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()}
+
+  let pretty () w =
+    Pretty.dprintf "{node = %a; prefix = %a; type_suffix = %a; type_suffix_prefix = %a}"
+      AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix
+end
+
+let group_may_race (warn_accs:WarnAccs.t) =
+  if M.tracing then M.tracei "access" "group_may_race %a\n" WarnAccs.pretty warn_accs;
   (* BFS to traverse one component with may_race edges *)
-  let rec bfs' ~ancestor_accs ~accs ~todo ~visited =
-    let may_race_accs ~accs ~todo =
+  let rec bfs' warn_accs ~todo ~visited =
+    let todo_all = WarnAccs.union_all todo in
+    let visited' = AS.union visited todo_all in (* Add all todo accesses to component. *)
+    let warn_accs' = WarnAccs.diff warn_accs todo in (* Todo accesses don't need to be considered as step targets, because they're already in the component. *)
+
+    let step_may_race ~todo ~accs = (* step from todo to accs if may_race *)
       AS.fold (fun acc todo' ->
           AS.fold (fun acc' todo' ->
               if may_race acc acc' then
@@ -392,30 +420,67 @@ let group_may_race ~ancestor_accs accs =
             ) accs todo'
         ) todo (AS.empty ())
     in
-    let accs' = AS.diff accs todo in
-    let ancestor_accs' = AS.diff ancestor_accs todo in
-    let todo_accs = may_race_accs ~accs:accs' ~todo in
-    let todo_ancestor_accs = may_race_accs ~accs:ancestor_accs' ~todo:(AS.diff todo ancestor_accs') in
-    let todo' = AS.union todo_accs todo_ancestor_accs in
-    let visited' = AS.union visited todo in
-    if AS.is_empty todo' then
-      (accs', visited')
+    (* Undirected graph of may_race checks:
+
+                type_suffix_prefix
+                        |
+                        |
+          type_suffix --+-- prefix
+                     \  |  /
+                      \ | /
+                       node
+                       / \
+                       \_/
+
+       Each undirected edge is handled by two opposite step_may_race-s.
+       All missing edges are checked at other nodes by other group_may_race calls. *)
+    let todo' : WarnAccs.t = {
+      node = step_may_race ~todo:todo_all ~accs:warn_accs'.node;
+      prefix = step_may_race ~todo:(AS.union todo.node todo.type_suffix) ~accs:warn_accs'.prefix;
+      type_suffix = step_may_race ~todo:(AS.union todo.node todo.prefix) ~accs:warn_accs'.type_suffix;
+      type_suffix_prefix = step_may_race ~todo:todo.node ~accs:warn_accs'.type_suffix_prefix
+    }
+    in
+
+    if WarnAccs.is_empty todo' then
+      (warn_accs', visited')
     else
-      (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~accs:accs' ~todo:todo' ~visited:visited'
+      (bfs' [@tailcall]) warn_accs' ~todo:todo' ~visited:visited'
   in
-  let bfs accs acc = bfs' ~ancestor_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in
-  (* repeat BFS to find all components *)
-  let rec components comps accs =
-    if AS.is_empty accs then
-      comps
+  let bfs warn_accs todo = bfs' warn_accs ~todo ~visited:(AS.empty ()) in
+  (* repeat BFS to find all components starting from node accesses *)
+  let rec components comps (warn_accs:WarnAccs.t) =
+    if AS.is_empty warn_accs.node then
+      (comps, warn_accs)
     else (
-      let acc = AS.choose accs in
-      let (accs', comp) = bfs accs acc in
+      let acc = AS.choose warn_accs.node in
+      let (warn_accs', comp) = bfs warn_accs {(WarnAccs.empty ()) with node=AS.singleton acc} in
       let comps' = comp :: comps in
-      components comps' accs'
+      components comps' warn_accs'
+    )
+  in
+  let (comps, warn_accs) = components [] warn_accs in
+  if M.tracing then M.trace "access" "components %a\n" WarnAccs.pretty warn_accs;
+  (* repeat BFS to find all prefix-type_suffix-only components starting from prefix accesses (symmetric) *)
+  let rec components_cross comps ~prefix ~type_suffix =
+    if AS.is_empty prefix then
+      comps
+    else (
+      let prefix_acc = AS.choose prefix in
+      let (warn_accs', comp) = bfs {(WarnAccs.empty ()) with prefix; type_suffix} {(WarnAccs.empty ()) with prefix=AS.singleton prefix_acc} in
+      if M.tracing then M.trace "access" "components_cross %a\n" WarnAccs.pretty warn_accs';
+      let comps' =
+        if AS.cardinal comp > 1 then
+          comp :: comps
+        else
+          comps (* ignore self-race prefix_acc component, self-race checked at prefix's level *)
+      in
+      components_cross comps' ~prefix:warn_accs'.prefix ~type_suffix:warn_accs'.type_suffix
     )
   in
-  components [] accs
+  let components_cross = components_cross comps ~prefix:warn_accs.prefix ~type_suffix:warn_accs.type_suffix in
+  if M.tracing then M.traceu "access" "group_may_race\n";
+  components_cross
 
 let race_conf accs =
   assert (not (AS.is_empty accs)); (* group_may_race should only construct non-empty components *)
@@ -483,7 +548,7 @@ let print_accesses memo grouped_accs =
         M.msg_group Success ?loc:group_loc ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs)
     )
 
-let warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo accs =
-  let grouped_accs = group_may_race ~ancestor_accs accs in (* do expensive component finding only once *)
+let warn_global ~safe ~vulnerable ~unsafe warn_accs memo =
+  let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *)
   incr_summary ~safe ~vulnerable ~unsafe grouped_accs;
   print_accesses memo grouped_accs
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index d0dcc428ad..c77d2cd738 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -359,6 +359,101 @@ let split_anoncomp_name name =
   else
     invalid_arg "Cilfacade.split_anoncomp_name"
 
+(** Pretty-print typsig like typ, because
+    {!d_typsig} prints with CIL constructors. *)
+let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
+  (* Copied & modified from Cil.defaultCilPrinterClass#pType. *)
+  let open Pretty in
+  let name = match nameOpt with None -> nil | Some d -> d in
+  let printAttributes (a: attributes) =
+    let pa = d_attrlist () a in
+    match nameOpt with
+    | None when not !print_CIL_Input ->
+      (* Cannot print the attributes in this case because gcc does not
+          like them here, except if we are printing for CIL. *)
+      if pa = nil then nil else
+        text "/*" ++ pa ++ text "*/"
+    | _ -> pa
+  in
+  match ts with
+  | TSBase t -> dn_type () t
+  | TSComp (cstruct, cname, a) ->
+    let su = if cstruct then "struct" else "union" in
+    text (su ^ " " ^ cname ^ " ")
+    ++ d_attrlist () a
+    ++ name
+  | TSEnum (ename, a) ->
+    text ("enum " ^ ename ^ " ")
+    ++ d_attrlist () a
+    ++ name
+  | TSPtr (bt, a)  ->
+    (* Parenthesize the ( * attr name) if a pointer to a function or an
+        array. *)
+    let (paren: doc option), (bt': typsig) =
+      match bt with
+      | TSFun _ | TSArray _ -> Some (text "("), bt
+      | _ -> None, bt
+    in
+    let name' = text "*" ++ printAttributes a ++ name in
+    let name'' = (* Put the parenthesis *)
+      match paren with
+        Some p -> p ++ name' ++ text ")"
+      | _ -> name'
+    in
+    pretty_typsig_like_typ
+      (Some name'')
+      ()
+      bt'
+
+  | TSArray (elemt, lo, a) ->
+    (* ignore the const attribute for arrays *)
+    let a' = dropAttributes [ "pconst" ] a in
+    let name' =
+      if a' == [] then name else
+      if nameOpt == None then printAttributes a' else
+        text "(" ++ printAttributes a' ++ name ++ text ")"
+    in
+    pretty_typsig_like_typ
+      (Some (name'
+             ++ text "["
+             ++ (match lo with None -> nil | Some e -> text (Z.to_string e))
+             ++ text "]"))
+      ()
+      elemt
+
+  | TSFun (restyp, args, isvararg, a) ->
+    let name' =
+      if a == [] then name else
+      if nameOpt == None then printAttributes a else
+        text "(" ++ printAttributes a ++ name ++ text ")"
+    in
+    pretty_typsig_like_typ
+      (Some
+         (name'
+          ++ text "("
+          ++ (align
+              ++
+              (if args = Some [] && isvararg then
+                 text "..."
+               else
+                 (if args = None then nil
+                  else if args = Some [] then text "void"
+                  else
+                    let pArg atype =
+                      (pretty_typsig_like_typ None () atype)
+                    in
+                    (docList ~sep:(chr ',' ++ break) pArg) ()
+                      (match args with None -> [] | Some args -> args))
+                 ++ (if isvararg then break ++ text ", ..." else nil))
+              ++ unalign)
+          ++ text ")"))
+      ()
+      restyp
+
+(** Pretty-print typsig like typ, because
+    {!d_typsig} prints with CIL constructors. *)
+let pretty_typsig_like_typ = pretty_typsig_like_typ None
+
 (** HashSet of line numbers *)
 let locs = Hashtbl.create 200
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 0e89ede0b5..1ef73378fb 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1284,7 +1284,8 @@
               "goblint",
               "sv-comp",
               "ncurses",
-              "zstd"
+              "zstd",
+              "pcre"
             ]
           },
           "default": [
diff --git a/tests/regression/04-mutex/49-type-invariants.c b/tests/regression/04-mutex/49-type-invariants.c
index 4f69986478..e6ac17dcd9 100644
--- a/tests/regression/04-mutex/49-type-invariants.c
+++ b/tests/regression/04-mutex/49-type-invariants.c
@@ -1,4 +1,3 @@
-//PARAM: --enable ana.race.direct-arithmetic
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t
index 3d3f7442ef..3ddd8f237d 100644
--- a/tests/regression/04-mutex/49-type-invariants.t
+++ b/tests/regression/04-mutex/49-type-invariants.t
@@ -1,47 +1,47 @@
   $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21)
-  [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11)
-    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:22:3-22:21)
-    read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:12:3-12:23)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
+  [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11)
+    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+    read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct S).field (safe):
-    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:22:3-22:21)
+    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:22:3-22:21)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:22:3-22:21)
-  [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:22:3-22:21)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:22:3-22:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:22:3-22:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:22:3-22:21)
-  [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:22:3-22:21)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21)
+  [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
 
   $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21)
-  [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11)
-    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:22:3-22:21)
-    read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:12:3-12:23)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
+  [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11)
+    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+    read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct S).field (safe):
-    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:22:3-22:21)
+    write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
     total lines: 7
-  [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:22:3-22:21)
-  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:22:3-22:21)
-  [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:22:3-22:21)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:22:3-22:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:22:3-22:21)
-  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:22:3-22:21)
-  [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:22:3-22:21)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21)
+  [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21)
diff --git a/tests/regression/04-mutex/77-type-nested-fields.c b/tests/regression/04-mutex/77-type-nested-fields.c
index 6f173d6fec..00b21e3fcf 100644
--- a/tests/regression/04-mutex/77-type-nested-fields.c
+++ b/tests/regression/04-mutex/77-type-nested-fields.c
@@ -1,7 +1,14 @@
-//PARAM: --enable ana.race.direct-arithmetic
 #include <pthread.h>
 #include <stdio.h>
 
+// (int)   (S)     (T)     (U)
+//    \   /   \   /   \   /
+//     >f<      s       t
+//        \   /   \   /
+//         >f<      s
+//            \   /
+//              f
+
 struct S {
   int field;
 };
diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t
new file mode 100644
index 0000000000..738784f5d5
--- /dev/null
+++ b/tests/regression/04-mutex/77-type-nested-fields.t
@@ -0,0 +1,29 @@
+  $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22)
+  [Warning][Race] Memory location (struct T).s.field (race with conf. 100):
+    write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+    write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 2
+  [Success][Race] Memory location (struct S).field (safe):
+    write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:31:3-31:20)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:31:3-31:20)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:38:3-38:22)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:38:3-38:22)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:38:3-38:22)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:38:3-38:22)
+  [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20)
+  [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22)
diff --git a/tests/regression/04-mutex/78-type-array.c b/tests/regression/04-mutex/78-type-array.c
index cdffe244b9..835f6163a3 100644
--- a/tests/regression/04-mutex/78-type-array.c
+++ b/tests/regression/04-mutex/78-type-array.c
@@ -1,4 +1,3 @@
-//PARAM: --enable ana.race.direct-arithmetic
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.c b/tests/regression/04-mutex/79-type-nested-fields-deep1.c
index ee99c40973..e100404960 100644
--- a/tests/regression/04-mutex/79-type-nested-fields-deep1.c
+++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.c
@@ -1,7 +1,14 @@
-//PARAM: --enable ana.race.direct-arithmetic
 #include <pthread.h>
 #include <stdio.h>
 
+// (int)   (S)     (T)     (U)
+//    \   /   \   /   \   /
+//     >f<      s       t
+//        \   /   \   /
+//          f       s
+//            \   /
+//             >f<
+
 struct S {
   int field;
 };
diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t
new file mode 100644
index 0000000000..2e15f83c39
--- /dev/null
+++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t
@@ -0,0 +1,29 @@
+  $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100):
+    write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+    write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 2
+  [Success][Race] Memory location (struct S).field (safe):
+    write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:43:3-43:24)
+  [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20)
+  [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24)
diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.c b/tests/regression/04-mutex/80-type-nested-fields-deep2.c
index 646acd9147..4ddd4684f7 100644
--- a/tests/regression/04-mutex/80-type-nested-fields-deep2.c
+++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.c
@@ -1,7 +1,14 @@
-//PARAM: --enable ana.race.direct-arithmetic
 #include <pthread.h>
 #include <stdio.h>
 
+// (int)   (S)     (T)     (U)
+//    \   /   \   /   \   /
+//      f       s       t
+//        \   /   \   /
+//         >f<      s
+//            \   /
+//             >f<
+
 struct S {
   int field;
 };
diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t
new file mode 100644
index 0000000000..48e726f623
--- /dev/null
+++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t
@@ -0,0 +1,29 @@
+  $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100):
+    write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+    write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 2
+  [Success][Race] Memory location (struct T).s.field (safe):
+    write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:43:3-43:24)
+  [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22)
+  [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24)
diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.c b/tests/regression/04-mutex/90-distribute-fields-type-1.c
new file mode 100644
index 0000000000..062b7421e6
--- /dev/null
+++ b/tests/regression/04-mutex/90-distribute-fields-type-1.c
@@ -0,0 +1,41 @@
+#include <pthread.h>
+#include <stdio.h>
+
+// (int)   (S)     (T)     (U)
+//    \   /   \   /   \   /
+//     >f<     >s<      t
+//        \   /   \   /
+//          f       s
+//            \   /
+//              f
+
+struct S {
+  int field;
+};
+
+struct T {
+  struct S s;
+};
+
+// struct S s;
+// struct T t;
+
+extern struct S* getS();
+extern struct T* getT();
+
+// getS could return the same struct as is contained in getT
+
+void *t_fun(void *arg) {
+  // should write to (struct T).s.field in addition to (struct S).field
+  // but easier to implement the other way around?
+  getS()->field = 1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  struct S s1;
+  getT()->s = s1; // RACE!
+  return 0;
+}
diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t
new file mode 100644
index 0000000000..ba3e3da0ed
--- /dev/null
+++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t
@@ -0,0 +1,31 @@
+  $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:31:3-31:20)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:39:3-39:17)
+  [Warning][Race] Memory location (struct T).s.field (race with conf. 100):
+    write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+    write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 3
+  [Success][Race] Memory location (struct S).field (safe):
+    write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+  [Success][Race] Memory location (struct T).s (safe):
+    write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:31:3-31:20)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:31:3-31:20)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:39:3-39:17)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:39:3-39:17)
+  [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20)
+  [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17)
diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.c b/tests/regression/04-mutex/91-distribute-fields-type-2.c
new file mode 100644
index 0000000000..01c945f730
--- /dev/null
+++ b/tests/regression/04-mutex/91-distribute-fields-type-2.c
@@ -0,0 +1,42 @@
+#include <pthread.h>
+#include <stdio.h>
+
+// (int)  >(S)<   >(T)<    (U)
+//    \   /   \   /   \   /
+//      f       s       t
+//        \   /   \   /
+//          f       s
+//            \   /
+//              f
+
+struct S {
+  int field;
+};
+
+struct T {
+  struct S s;
+};
+
+// struct S s;
+// struct T t;
+
+extern struct S* getS();
+extern struct T* getT();
+
+// getS could return the same struct as is contained in getT
+
+void *t_fun(void *arg) {
+  // should write to (struct T).s.field in addition to (struct S).field
+  // but easier to implement the other way around?
+  struct S s1;
+  *(getS()) = s1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  struct T t1;
+  *(getT()) = t1; // RACE!
+  return 0;
+}
diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t
new file mode 100644
index 0000000000..fd544b0b0b
--- /dev/null
+++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t
@@ -0,0 +1,31 @@
+  $ goblint --enable warn.deterministic --enable allglobs 91-distribute-fields-type-2.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:32:3-32:17)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:40:3-40:17)
+  [Warning][Race] Memory location (struct T).s (race with conf. 100):
+    write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+    write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 3
+  [Success][Race] Memory location (struct S) (safe):
+    write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+  [Success][Race] Memory location (struct T) (safe):
+    write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:32:3-32:17)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:32:3-32:17)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:40:3-40:17)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:40:3-40:17)
+  [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17)
+  [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17)
diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.c b/tests/regression/04-mutex/92-distribute-fields-type-deep.c
new file mode 100644
index 0000000000..59fb09a605
--- /dev/null
+++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.c
@@ -0,0 +1,46 @@
+#include <pthread.h>
+#include <stdio.h>
+
+// (int)   (S)     (T)     (U)
+//    \   /   \   /   \   /
+//     >f<      s      >t<
+//        \   /   \   /
+//          f       s
+//            \   /
+//              f
+
+struct S {
+  int field;
+};
+
+struct T {
+  struct S s;
+};
+
+struct U {
+  struct T t;
+};
+
+// struct S s;
+// struct T t;
+
+extern struct S* getS();
+extern struct T* getT();
+extern struct U* getU();
+
+// getS could return the same struct as is contained in getT
+
+void *t_fun(void *arg) {
+  // should write to (struct U).t.s.field in addition to (struct T).s.field
+  // but easier to implement the other way around?
+  getS()->field = 1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  struct T t1;
+  getU()->t = t1; // RACE!
+  return 0;
+}
diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t
new file mode 100644
index 0000000000..aefc1520d1
--- /dev/null
+++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t
@@ -0,0 +1,31 @@
+  $ goblint --enable warn.deterministic --enable allglobs 92-distribute-fields-type-deep.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100):
+    write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+    write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 3
+  [Success][Race] Memory location (struct S).field (safe):
+    write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Success][Race] Memory location (struct U).t (safe):
+    write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:44:3-44:17)
+  [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20)
+  [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17)
diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.c b/tests/regression/04-mutex/93-distribute-fields-type-global.c
new file mode 100644
index 0000000000..466d47e7fc
--- /dev/null
+++ b/tests/regression/04-mutex/93-distribute-fields-type-global.c
@@ -0,0 +1,25 @@
+#include <pthread.h>
+#include <stdio.h>
+
+struct S {
+  int field;
+};
+
+struct S s;
+
+extern struct S* getS();
+
+void *t_fun(void *arg) {
+  printf("%d",getS()->field); // RACE!
+
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  struct S s1;
+  s = s1; // RACE!
+  return 0;
+}
+
diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t
new file mode 100644
index 0000000000..2199c689b1
--- /dev/null
+++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t
@@ -0,0 +1,25 @@
+  $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:13:3-13:29)
+  [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:8:10-8:11)
+    read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+    write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 3
+  [Success][Race] Memory location (struct S).field (safe):
+    read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+  [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:8:10-8:11)
+    write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29)
+  [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29)
+  [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29)
diff --git a/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/94-thread-unsafe_fun_rc.c
similarity index 100%
rename from tests/regression/04-mutex/90-thread-unsafe_fun_rc.c
rename to tests/regression/04-mutex/94-thread-unsafe_fun_rc.c
diff --git a/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/95-thread-unsafe_fun_nr.c
similarity index 100%
rename from tests/regression/04-mutex/91-thread-unsafe_fun_nr.c
rename to tests/regression/04-mutex/95-thread-unsafe_fun_nr.c
diff --git a/tests/regression/06-symbeq/16-type_rc.c b/tests/regression/06-symbeq/16-type_rc.c
index efeb6c768b..e9e7c7972b 100644
--- a/tests/regression/06-symbeq/16-type_rc.c
+++ b/tests/regression/06-symbeq/16-type_rc.c
@@ -1,6 +1,14 @@
 // PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
 #include<pthread.h>
 
+//>(int)<  (S)     (T)     (U)
+//    \   /   \   /   \   / 
+//     >f<      s       t
+//        \   /   \   /  
+//          f       s
+//            \   /
+//              f
+
 struct s {
   int datum;
   pthread_mutex_t mutex;
diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t
index 78c293b7ef..06a3b314a4 100644
--- a/tests/regression/06-symbeq/16-type_rc.t
+++ b/tests/regression/06-symbeq/16-type_rc.t
@@ -1,22 +1,22 @@
 Disable info messages because race summary contains (safe) memory location count, which is different on Linux and OSX.
 
   $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" 16-type_rc.c
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:13:3-13:15)
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:24:3-24:16)
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:25:3-25:16)
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:28:3-28:9)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9)
   [Warning][Race] Memory location (struct s).datum (race with conf. 100):
-    write with [mhp:{tid=[main, t_fun@16-type_rc.c:27:3-27:37#top]}, thread:[main, t_fun@16-type_rc.c:27:3-27:37#top]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:13:3-13:15)
-    write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:27:3-27:37#top]}}, thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:28:3-28:9)
-  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:12:12-12:24)
-  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:23:3-23:14)
+    write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+    write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
+  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24)
+  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)
 
   $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:13:3-13:15)
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:24:3-24:16)
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:25:3-25:16)
-  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:28:3-28:9)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9)
   [Success][Race] Memory location (struct s).datum (safe):
-    write with [mhp:{tid=[main, t_fun@16-type_rc.c:27:3-27:37#top]}, thread:[main, t_fun@16-type_rc.c:27:3-27:37#top]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:13:3-13:15)
-  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:12:12-12:24)
-  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:23:3-23:14)
+    write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24)
+  [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)