diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 9b6230350..28996379c 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -393,11 +393,15 @@ let pp_specs pe fmt specs =
   let cnt = ref 0 in
   match pe.Pp.kind with
   | TEXT ->
-      IList.iter (fun spec -> incr cnt; F.fprintf fmt "%a@\n" (pp_spec pe (Some (!cnt, total))) spec) specs
+      IList.iter (fun spec -> incr cnt;
+                   F.fprintf fmt "%a" (pp_spec pe (Some (!cnt, total))) spec) specs
   | HTML ->
-      IList.iter (fun spec -> incr cnt; F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (!cnt, total))) spec) specs
+      IList.iter (fun spec -> incr cnt;
+                   F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (!cnt, total))) spec) specs
   | LATEX ->
-      IList.iter (fun spec -> incr cnt; F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n" !cnt total (pp_spec pe None) spec) specs
+      IList.iter (fun spec -> incr cnt;
+                   F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n"
+                     !cnt total (pp_spec pe None) spec) specs
 
 (** Print the decpendency map *)
 let pp_dependency_map fmt dependency_map =
@@ -450,7 +454,7 @@ let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof;
   let pp_opt pp fmt = function
     | Some x -> pp fmt x
     | None -> () in
-  F.fprintf fmt "%a%a%a%a%a%a"
+  F.fprintf fmt "%a%a%a%a%a%a@\n"
     (pp_specs pe) (get_specs_from_preposts preposts)
     (pp_opt (TypeState.pp TypeState.unit_ext)) typestate
     (pp_opt Crashcontext.pp_stacktree) crashcontext_frame
diff --git a/infer/src/checkers/SinkTrace.ml b/infer/src/checkers/SinkTrace.ml
index 09cde50f7..985fe6a36 100644
--- a/infer/src/checkers/SinkTrace.ml
+++ b/infer/src/checkers/SinkTrace.ml
@@ -63,4 +63,13 @@ module Make (TraceElem : TraceElem.S) = struct
          add_sink callee_sink t_acc)
       initial
       (Sinks.elements (sinks t))
+
+  let pp fmt t =
+    let pp_passthroughs_if_not_empty fmt p =
+      if not (Passthroughs.is_empty p) then
+        F.fprintf fmt " via %a" Passthroughs.pp p in
+    F.fprintf
+      fmt
+      "%a%a"
+      Sinks.pp (sinks t) pp_passthroughs_if_not_empty (passthroughs t)
 end
diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml
index 12ea45e4d..4ab565020 100644
--- a/infer/src/checkers/Siof.ml
+++ b/infer/src/checkers/Siof.ml
@@ -12,6 +12,8 @@ open! IStd
 module F = Format
 module L = Logging
 
+module GlobalsAccesses = SiofTrace.GlobalsAccesses
+
 module Summary = Summary.Make (struct
     type summary = SiofDomain.astate
 
@@ -37,40 +39,44 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | _ ->
         false
 
-  let get_globals astate pdesc loc e =
+  let get_globals pdesc loc e =
     let is_dangerous_global pv =
       Pvar.is_global pv
       && not (Pvar.is_static_local pv)
       && not (Pvar.is_pod pv)
       && not (Pvar.is_compile_constant pv)
       && not (is_compile_time_constructed pdesc pv) in
-    let globals = Exp.get_vars e |> snd |> IList.filter is_dangerous_global in
-    if globals = [] then
-      Domain.Bottom
+    let globals_accesses =
+      Exp.get_vars e |> snd |> IList.filter is_dangerous_global
+      |> IList.map (fun v -> (v, loc)) in
+    GlobalsAccesses.of_list globals_accesses
+
+  let add_globals astate outer_loc globals =
+    if GlobalsAccesses.is_empty globals then
+      astate
     else
       let trace = match astate with
         | Domain.Bottom -> SiofTrace.initial
         | Domain.NonBottom t -> t in
       let globals_trace =
-        IList.fold_left (fun trace_acc global ->
-            SiofTrace.add_sink (SiofTrace.make_access global loc) trace_acc)
-          trace
-          globals in
+        SiofTrace.add_sink (SiofTrace.make_access globals outer_loc) trace in
       Domain.NonBottom globals_trace
 
-  let add_params_globals astate pdesc loc params =
-    IList.map fst params
-    |> IList.map (fun e -> get_globals astate pdesc loc e)
-    |> IList.fold_left Domain.join astate
+  let add_params_globals astate pdesc call_loc params =
+    IList.map (fun (e, _) -> get_globals pdesc call_loc e) params
+    |> IList.fold_left GlobalsAccesses.union GlobalsAccesses.empty
+    |> add_globals astate (Procdesc.get_loc pdesc)
 
-  let at_least_bottom =
+  let at_least_nonbottom =
     Domain.join (Domain.NonBottom SiofTrace.initial)
 
-  let exec_instr astate { ProcData.pdesc; } _ (instr : Sil.instr) = match instr with
+  let exec_instr astate { ProcData.pdesc; } _ (instr : Sil.instr) =
+    match instr with
     | Load (_, exp, _, loc)
     | Store (_, _, exp, loc)
     | Prune (exp, loc, _, _) ->
-        Domain.join astate (get_globals astate pdesc loc exp)
+        let proc_loc = Procdesc.get_loc pdesc in
+        get_globals pdesc loc exp |> add_globals astate proc_loc
     | Call (_, Const (Cfun callee_pname), _::params_without_self, loc, _)
       when Procname.is_c_method callee_pname && Procname.is_constructor callee_pname
            && Procname.is_constexpr callee_pname ->
@@ -81,18 +87,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           match Summary.read_summary pdesc callee_pname with
           | Some (Domain.NonBottom trace) ->
               Domain.NonBottom (SiofTrace.with_callsite trace callsite)
-          | _ ->
+          | None | Some Domain.Bottom ->
               Domain.Bottom in
         add_params_globals astate pdesc loc params
         |> Domain.join callee_globals
         |>
         (* make sure it's not Bottom: we made a function call so this needs initialization *)
-        at_least_bottom
+        at_least_nonbottom
     | Call (_, _, params, loc, _) ->
         add_params_globals astate pdesc loc params
         |>
         (* make sure it's not Bottom: we made a function call so this needs initialization *)
-        at_least_bottom
+        at_least_nonbottom
     | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ ->
         astate
 end
@@ -106,7 +112,7 @@ module Analyzer =
 module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
 
 
-let is_foreign tu_opt v =
+let is_foreign tu_opt (v, _) =
   let is_orig_file f = match tu_opt with
     | Some orig_file ->
         let orig_path = SourceFile.to_abs_path orig_file in
@@ -123,62 +129,59 @@ let report_siof trace pdesc gname loc =
     | Some (SiofDomain.NonBottom summary) -> summary
     | _ -> SiofTrace.initial in
 
-  let pp_sink f sink =
-    let pp_source f v = match Pvar.get_source_file v with
-      | Some source_file when not (SourceFile.equal SourceFile.empty source_file) ->
-          F.fprintf f " from file %a" SourceFile.pp source_file
-      | _ ->
-          () in
-    let v = SiofTrace.Sink.kind sink in
-    F.fprintf f "%s%a" (Pvar.get_simplified_name v) pp_source v in
-
-  let trace_of_error path =
-    let desc_of_sink sink =
-      let callsite = SiofTrace.Sink.call_site sink in
-      if SiofTrace.is_intraprocedural_access sink then
-        Format.asprintf "access to %s" (Pvar.get_simplified_name (SiofTrace.Sink.kind sink))
-      else
-        Format.asprintf "call to %a" Procname.pp (CallSite.pname callsite) in
-    let sink_should_nest sink = not (SiofTrace.is_intraprocedural_access sink) in
-    let trace_elem_of_global =
-      Errlog.make_trace_element 0 loc
-        (Format.asprintf "initialization of %s" gname)
-        [] in
-    trace_elem_of_global::(SiofTrace.to_sink_loc_trace ~desc_of_sink ~sink_should_nest path) in
-
-  let report_one_path ((_, path) as sink_path) =
-    let final_sink = fst (IList.hd path) in
-    if is_foreign tu_opt (SiofTrace.Sink.kind final_sink) then (
-      let description =
-        F.asprintf
-          "The initializer of %s accesses global variables in another translation unit: %a"
-          gname
-          pp_sink final_sink in
-      let ltr = trace_of_error sink_path in
-      let caller_pname = Procdesc.get_proc_name pdesc in
-      let msg = Localise.to_string Localise.static_initialization_order_fiasco in
-      let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in
-      Reporting.log_error caller_pname ~loc ~ltr exn
-    ); in
-
-  IList.iter report_one_path (SiofTrace.get_reportable_sink_paths trace ~trace_of_pname)
+  let report_one_path (passthroughs, path) =
+    let description, sink_path' = match path with
+      | [] -> assert false
+      | (final_sink, pt)::rest ->
+          let foreign_globals =
+            SiofTrace.Sink.kind final_sink |> GlobalsAccesses.filter (is_foreign tu_opt) in
+          let final_sink' =
+            let loc = CallSite.loc (SiofTrace.Sink.call_site final_sink) in
+            SiofTrace.make_access foreign_globals loc in
+          let description =
+            F.asprintf
+              "Initializer of %s accesses global variables from a different translation unit: %a"
+              gname
+              GlobalsAccesses.pp foreign_globals in
+          description, (passthroughs, (final_sink', pt)::rest) in
+    let ltr = SiofTrace.trace_of_error loc gname sink_path' in
+    let caller_pname = Procdesc.get_proc_name pdesc in
+    let msg = Localise.to_string Localise.static_initialization_order_fiasco in
+    let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in
+    Reporting.log_error caller_pname ~loc ~ltr exn in
+
+  let has_foreign_sink (_, path) =
+    IList.exists
+      (fun (sink, _) ->
+         GlobalsAccesses.exists (is_foreign tu_opt)
+           (SiofTrace.Sink.kind sink))
+      path in
+
+  SiofTrace.get_reportable_sink_paths trace ~trace_of_pname
+  |> IList.filter has_foreign_sink
+  |> IList.iter report_one_path
 
 let siof_check pdesc gname = function
   | Some (SiofDomain.NonBottom post) ->
       let attrs = Procdesc.get_attributes pdesc in
-      let foreign_global_sinks =
-        SiofTrace.Sinks.filter
-          (fun sink -> is_foreign attrs.ProcAttributes.translation_unit (SiofTrace.Sink.kind sink))
-          (SiofTrace.sinks post) in
-      if not (SiofTrace.Sinks.is_empty foreign_global_sinks)
-      then report_siof post pdesc gname attrs.ProcAttributes.loc;
+      let all_globals = SiofTrace.Sinks.fold
+          (fun sink -> GlobalsAccesses.union (SiofTrace.Sink.kind sink))
+          (SiofTrace.sinks post) GlobalsAccesses.empty in
+      let tu_opt =
+        let attrs = Procdesc.get_attributes pdesc in
+        attrs.ProcAttributes.translation_unit in
+      if GlobalsAccesses.exists (is_foreign tu_opt) all_globals then
+        report_siof post pdesc gname attrs.ProcAttributes.loc;
   | Some SiofDomain.Bottom | None ->
       ()
 
+let compute_post proc_data =
+  Analyzer.compute_post proc_data |> Option.map ~f:SiofDomain.normalize
+
 let checker ({ Callbacks.proc_desc; } as callback) =
   let post =
     Interprocedural.compute_and_store_post
-      ~compute_post:Analyzer.compute_post
+      ~compute_post
       ~make_extras:ProcData.make_empty_extras
       callback in
   let pname = Procdesc.get_proc_name proc_desc in
diff --git a/infer/src/checkers/SiofDomain.ml b/infer/src/checkers/SiofDomain.ml
index c41e345d2..7b2becb97 100644
--- a/infer/src/checkers/SiofDomain.ml
+++ b/infer/src/checkers/SiofDomain.ml
@@ -20,3 +20,24 @@ open! IStd
    initialization, and which globals requiring initialization a given function (transitively)
    accesses. *)
 include AbstractDomain.BottomLifted(SiofTrace)
+
+(** group together procedure-local accesses *)
+let normalize astate = match astate with
+  | Bottom -> astate
+  | NonBottom trace ->
+      let elems = SiofTrace.Sinks.elements (SiofTrace.sinks trace) in
+      let (direct, indirect) = IList.partition SiofTrace.is_intraprocedural_access elems in
+      match direct with
+      | [] | _::[] -> astate
+      | access::_ ->
+          (* [loc] should be the same for all local accesses: it's the loc of the enclosing
+             procdesc. Use the loc of the first access. *)
+          let loc = CallSite.loc (SiofTrace.Sink.call_site access) in
+          let kind =
+            IList.map SiofTrace.Sink.kind direct
+            |> IList.fold_left SiofTrace.GlobalsAccesses.union SiofTrace.GlobalsAccesses.empty in
+          let trace' =
+            SiofTrace.make_access kind loc::indirect
+            |> SiofTrace.Sinks.of_list
+            |> SiofTrace.update_sinks trace in
+          NonBottom trace'
diff --git a/infer/src/checkers/SiofDomain.mli b/infer/src/checkers/SiofDomain.mli
new file mode 100644
index 000000000..c67c36e99
--- /dev/null
+++ b/infer/src/checkers/SiofDomain.mli
@@ -0,0 +1,23 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(* The domain for the analysis is sets of global variables if an initialization is needed at
+   runtime, or Bottom if no initialization is needed. For instance, `int x = 32; int y = x * 52;`
+   gives a summary of Bottom for both initializers corresponding to these globals, but `int x =
+   foo();` gives a summary of at least "NonBottom {}" for x's initializer since x will need runtime
+   initialization.
+
+   The encoding in terms of a BottomLifted domain is an efficiency hack to represent two pieces of
+   information: whether a global variable (via its initializer function) requires runtime
+   initialization, and which globals requiring initialization a given function (transitively)
+   accesses. *)
+include module type of (AbstractDomain.BottomLifted(SiofTrace))
+
+(** group together procedure-local accesses *)
+val normalize : astate -> astate
diff --git a/infer/src/checkers/SiofTrace.ml b/infer/src/checkers/SiofTrace.ml
index 15b94bdc3..0347adf33 100644
--- a/infer/src/checkers/SiofTrace.ml
+++ b/infer/src/checkers/SiofTrace.ml
@@ -12,14 +12,20 @@ open! IStd
 module F = Format
 module L = Logging
 
-module Global = struct
-  type t = Pvar.t
-  let compare = Pvar.compare
-  let pp fmt pvar = (Pvar.pp Pp.text) fmt pvar
-end
+module GlobalsAccesses = PrettyPrintable.MakePPSet (struct
+    type t = (Pvar.t * Location.t)
+    let compare (v1, l1) (v2, l2) =
+      (* compare by loc first to present reports in the right order *)
+      [%compare : (Location.t * Pvar.t)] (l1, v1) (l2, v2)
+    let pp_element fmt (v, _) =
+      F.fprintf fmt "%a" Mangled.pp (Pvar.get_name v);
+      match Pvar.get_source_file v with
+      | Some fname -> F.fprintf fmt "%a" SourceFile.pp fname
+      | None -> ()
+  end)
 
 module TraceElem = struct
-  module Kind = Global
+  module Kind = GlobalsAccesses
 
   type t = {
     site : CallSite.t;
@@ -35,9 +41,16 @@ module TraceElem = struct
   let with_callsite { kind=(_, kind); } site = { kind=(`Call, kind); site; }
 
   let pp fmt { site; kind; } =
-    F.fprintf fmt "Access to %a at %a" Kind.pp (snd kind) CallSite.pp site
+    F.fprintf fmt "%saccess to %a"
+      (match fst kind with | `Call -> "indirect " | `Access -> "")
+      Kind.pp (snd kind);
+    match fst kind with
+    | `Call -> F.fprintf fmt " at %a" CallSite.pp site
+    | `Access -> ()
 
   module Set = PrettyPrintable.MakePPSet (struct
+      (* Don't use nonrec due to https://github.com/janestreet/ppx_compare/issues/2 *)
+      (* type nonrec t = t [@@deriving compare]; *)
       type nonrec t = t
       let compare = compare
       let pp_element = pp
@@ -52,3 +65,35 @@ let make_access kind loc =
   { TraceElem.kind = (`Access, kind); site; }
 
 let is_intraprocedural_access { TraceElem.kind=(kind, _); } = kind = `Access
+
+let trace_of_error loc gname path =
+  let desc_of_sink sink =
+    let callsite = Sink.call_site sink in
+    if is_intraprocedural_access sink then
+      Format.asprintf "%a" Sink.pp sink
+    else
+      Format.asprintf "call to %a" Procname.pp (CallSite.pname callsite) in
+  let sink_should_nest sink = not (is_intraprocedural_access sink) in
+  let trace_elem_of_global =
+    Errlog.make_trace_element 0 loc
+      (Format.asprintf "initialization of %s" gname)
+      [] in
+  let trace =
+    let trace_with_set_of_globals = to_sink_loc_trace ~desc_of_sink ~sink_should_nest path in
+    (* the last element of the trace gotten by [to_sink_loc_trace] contains a set of procedure-local
+       accesses to globals. We want to remove it in exchange for as many trace elems as there are
+       accesses. *)
+    match (IList.rev trace_with_set_of_globals, snd path) with
+    | telem::rest, ({TraceElem.kind = (`Access, globals)}, _)::_ ->
+        let nesting = telem.Errlog.lt_level in
+        let add_trace_elem_of_access err_trace (global, loc) =
+          Errlog.make_trace_element nesting loc
+            (Format.asprintf "access to %a" Mangled.pp (Pvar.get_name global))
+            []
+          ::err_trace in
+        GlobalsAccesses.elements globals
+        |> IList.fold_left add_trace_elem_of_access rest
+        |> IList.rev
+    | _ -> trace_with_set_of_globals
+  in
+  trace_elem_of_global::trace
diff --git a/infer/src/checkers/SiofTrace.mli b/infer/src/checkers/SiofTrace.mli
index 452277543..a891e8225 100644
--- a/infer/src/checkers/SiofTrace.mli
+++ b/infer/src/checkers/SiofTrace.mli
@@ -9,15 +9,12 @@
 
 open! IStd
 
-module Global :
-sig
-  type t = Pvar.t
-  val compare : t -> t -> int
-  val pp : Format.formatter -> t -> unit
-end
+module GlobalsAccesses : PrettyPrintable.PPSet with type elt = (Pvar.t * Location.t)
 
-include SinkTrace.S with module Sink.Kind = Global
+include SinkTrace.S with type Sink.Kind.t = GlobalsAccesses.t
 
-val make_access : Global.t -> Location.t -> Sink.t
+val make_access : GlobalsAccesses.t -> Location.t -> Sink.t
 
 val is_intraprocedural_access : Sink.t -> bool
+
+val trace_of_error : Location.t -> string -> sink_path -> Errlog.loc_trace_elem list
diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml
index 430c47237..8fc59ad0b 100644
--- a/infer/src/checkers/Trace.ml
+++ b/infer/src/checkers/Trace.ml
@@ -70,6 +70,8 @@ module type S = sig
   (** add a sink to the current trace. *)
   val add_sink : Sink.t -> t -> t
 
+  val update_sinks : t -> Sinks.t -> t
+
   (** append the trace for given call site to the current caller trace *)
   val append : t -> t -> CallSite.t -> t
 
@@ -334,6 +336,8 @@ module Make (Spec : Spec) = struct
     let sinks = Sinks.add sink t.sinks in
     { t with sinks; }
 
+  let update_sinks t sinks = { t with sinks }
+
   (** compute caller_trace + callee_trace *)
   let append caller_trace callee_trace callee_site =
     if is_empty callee_trace
diff --git a/infer/src/checkers/Trace.mli b/infer/src/checkers/Trace.mli
index a2f3fe791..29e388b9f 100644
--- a/infer/src/checkers/Trace.mli
+++ b/infer/src/checkers/Trace.mli
@@ -70,6 +70,9 @@ module type S = sig
   (** add a sink to the current trace. *)
   val add_sink : Sink.t -> t -> t
 
+  (** replace sinks with new ones *)
+  val update_sinks : t -> Sinks.t -> t
+
   (** append the trace for given call site to the current caller trace *)
   val append : t -> t -> CallSite.t -> t
 
diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml
index 285bc5a94..be05f1812 100644
--- a/infer/src/checkers/summary.ml
+++ b/infer/src/checkers/summary.ml
@@ -13,25 +13,24 @@ module type Helper = sig
   type summary
   (*  type astate*)
 
-  (* update the specs payload with [summary] *)
+  (** update the specs payload with [summary] *)
   val update_payload : summary -> Specs.payload -> Specs.payload
-  (* extract [summmary] from the specs payload *)
-  val read_from_payload : Specs.payload -> summary option
 
-  (*val to_summary : astate -> summary*)
+  (** extract [summmary] from the specs payload *)
+  val read_from_payload : Specs.payload -> summary option
 end
 
 module type S = sig
   type summary
   (*  type astate*)
 
-  (* write the summary for [name] to persistent storage *)
+  (** Write the [summary] for the procname to persistent storage. Returns the summary actually
+      written. *)
   val write_summary : Procname.t -> summary -> unit
-  (* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to
-     create the summary if needed *)
-  val read_summary : Procdesc.t -> Procname.t -> summary option
 
-  (*  val to_summary : astate -> summary*)
+  (** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis
+      to create the summary if needed *)
+  val read_summary : Procdesc.t -> Procname.t -> summary option
 end
 
 module Make (H : Helper) = struct
diff --git a/infer/src/checkers/summary.mli b/infer/src/checkers/summary.mli
new file mode 100644
index 000000000..2a0a5ce04
--- /dev/null
+++ b/infer/src/checkers/summary.mli
@@ -0,0 +1,33 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module type Helper = sig
+  type summary
+
+  (** update the specs payload with [summary] *)
+  val update_payload : summary -> Specs.payload -> Specs.payload
+
+  (** extract [summmary] from the specs payload *)
+  val read_from_payload : Specs.payload -> summary option
+end
+
+module type S = sig
+  type summary
+
+  (** Write the [summary] for the procname to persistent storage. Returns the summary actually
+      written. *)
+  val write_summary : Procname.t -> summary -> unit
+
+  (** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis
+      to create the summary if needed *)
+  val read_summary : Procdesc.t -> Procname.t -> summary option
+
+end
+
+module Make (H : Helper) : S with type summary = H.summary
diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml
index cfec4b57a..e79d392ca 100644
--- a/infer/src/checkers/transferFunctions.ml
+++ b/infer/src/checkers/transferFunctions.ml
@@ -14,10 +14,14 @@ open! IStd
 
 module type S = sig
   module CFG : ProcCfg.S
-  module Domain : AbstractDomain.S (* abstract domain whose state we propagate *)
-  type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
 
-  (* {A} instr {A'}. [node] is the node of the current instruction *)
+  (** abstract domain whose state we propagate *)
+  module Domain : AbstractDomain.S
+
+  (** read-only extra state (results of previous analyses, globals, etc.) *)
+  type extras
+
+  (** {A} instr {A'}. [node] is the node of the current instruction *)
   val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
 end
 
diff --git a/infer/src/checkers/transferFunctions.mli b/infer/src/checkers/transferFunctions.mli
index cfec4b57a..e79d392ca 100644
--- a/infer/src/checkers/transferFunctions.mli
+++ b/infer/src/checkers/transferFunctions.mli
@@ -14,10 +14,14 @@ open! IStd
 
 module type S = sig
   module CFG : ProcCfg.S
-  module Domain : AbstractDomain.S (* abstract domain whose state we propagate *)
-  type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
 
-  (* {A} instr {A'}. [node] is the node of the current instruction *)
+  (** abstract domain whose state we propagate *)
+  module Domain : AbstractDomain.S
+
+  (** read-only extra state (results of previous analyses, globals, etc.) *)
+  type extras
+
+  (** {A} instr {A'}. [node] is the node of the current instruction *)
   val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
 end
 
diff --git a/infer/tests/codetoanalyze/cpp/checkers/issues.exp b/infer/tests/codetoanalyze/cpp/checkers/issues.exp
index fc5c5f10e..d8f3ec4fb 100644
--- a/infer/tests/codetoanalyze/cpp/checkers/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/checkers/issues.exp
@@ -1,9 +1,9 @@
-codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_X::static_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of X::static_pod_accesses_non_pod,call to access_to_non_pod,access to global_object2]
+codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_X::static_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of X::static_pod_accesses_non_pod,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
 codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object,call to SomeOtherNonPODObject_SomeOtherNonPODObject,access to extern_global_object]
-codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object2,call to access_to_non_pod,access to global_object2]
+codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object2,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
 codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object3, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object3,call to access_to_templated_non_pod,access to global_object3]
-codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_initWithGlobal, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of initWithGlobal,call to getGlobalNonPOD,access to global_object2]
-codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of pod_accesses_non_pod,call to access_to_non_pod,access to global_object2]
+codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_initWithGlobal, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of initWithGlobal,call to getGlobalNonPOD,access to some_other_global_object2,access to global_object2]
+codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of pod_accesses_non_pod,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
 codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object,call to SomeOtherTemplatedNonPODObject<_Bool>_SomeOtherTemplatedNonPODObject,access to extern_global_object]
-codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object2,call to access_to_non_pod,access to global_object2]
+codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object2,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
 codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object3, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object3,call to access_to_templated_non_pod,access to global_object3]
diff --git a/infer/tests/codetoanalyze/cpp/checkers/siof/siof_different_tu.cpp b/infer/tests/codetoanalyze/cpp/checkers/siof/siof_different_tu.cpp
index 5809ad90d..cf7931766 100644
--- a/infer/tests/codetoanalyze/cpp/checkers/siof/siof_different_tu.cpp
+++ b/infer/tests/codetoanalyze/cpp/checkers/siof/siof_different_tu.cpp
@@ -10,9 +10,12 @@
 #include "siof_types.h"
 
 SomeNonPODObject global_object2;
+SomeNonPODObject some_other_global_object2;
 
 int access_to_non_pod() {
   global_object2.some_method();
+  // access several global objects to check that we group the reports together
+  some_other_global_object2.some_method();
   return 5;
 }
 
@@ -25,7 +28,10 @@ SomeNonPODObject& getFunctionStaticNonPOD() {
   return instance;
 }
 
-SomeNonPODObject& getGlobalNonPOD() { return global_object2; }
+SomeNonPODObject& getGlobalNonPOD() {
+  some_other_global_object2.some_method();
+  return global_object2;
+}
 
 // initialise static class field
 SomeConstexprObject SomeConstexprObject::instance_;