diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli
index 83950555d..c7ec4ff75 100644
--- a/infer/src/IR/HilInstr.mli
+++ b/infer/src/IR/HilInstr.mli
@@ -11,6 +11,8 @@ module F = Format
 (** type of a procedure call; either direct or via function pointer *)
 type call = Direct of Typ.Procname.t | Indirect of HilExp.AccessExpression.t [@@deriving compare]
 
+val pp_call : F.formatter -> call -> unit
+
 type t =
   | Assign of HilExp.AccessExpression.t * HilExp.t * Location.t
       (** LHS access expression, RHS expression *)
diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml
index ef9523136..5fd0e293e 100644
--- a/infer/src/IR/Pvar.ml
+++ b/infer/src/IR/Pvar.ml
@@ -108,7 +108,7 @@ let get_simplified_name pv =
   let s = Mangled.to_string pv.pv_name in
   match String.rsplit2 s ~on:'.' with
   | Some (s1, s2) -> (
-    match String.rsplit2 s1 ~on:'.' with Some (_, s4) -> s4 ^ "." ^ s2 | _ -> s )
+    match String.rsplit2 s1 ~on:'.' with Some (_, s4) -> Printf.sprintf "%s.%s" s4 s2 | _ -> s )
   | _ ->
       s
 
diff --git a/infer/src/base/Location.ml b/infer/src/base/Location.ml
index aabe7a6a3..52d1467e9 100644
--- a/infer/src/base/Location.ml
+++ b/infer/src/base/Location.ml
@@ -20,9 +20,11 @@ let none file = {line= -1; col= -1; file}
 
 let dummy = none (SourceFile.invalid __FILE__)
 
+let pp_line f loc = F.fprintf f "line %d" loc.line
+
 (** Pretty print a location *)
 let pp f (loc : t) =
-  F.fprintf f "line %d" loc.line ;
+  pp_line f loc ;
   if loc.col <> -1 then F.fprintf f ", column %d" loc.col
 
 
diff --git a/infer/src/base/Location.mli b/infer/src/base/Location.mli
index 4a66fffda..469981a75 100644
--- a/infer/src/base/Location.mli
+++ b/infer/src/base/Location.mli
@@ -25,6 +25,9 @@ val dummy : t
 val pp : Format.formatter -> t -> unit
 (** Pretty print a location. *)
 
+val pp_line : Format.formatter -> t -> unit
+(** print just the line information *)
+
 val to_string : t -> string
 (** String representation of a location. *)
 
diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml
index 379f94855..21d809c76 100644
--- a/infer/src/checkers/Pulse.ml
+++ b/infer/src/checkers/Pulse.ml
@@ -44,15 +44,17 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
   let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc
       astate =
     (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *)
+    let crumb = PulseTrace.Assignment {lhs= lhs_access; location= loc} in
     match rhs_exp with
     | AccessExpression rhs_access -> (
         PulseDomain.read loc rhs_access astate
-        >>= fun (astate, rhs_value) ->
-        PulseDomain.write loc lhs_access rhs_value astate
+        >>= fun (astate, (rhs_addr, rhs_trace)) ->
+        let return_addr_trace = (rhs_addr, crumb :: rhs_trace) in
+        PulseDomain.write loc lhs_access return_addr_trace astate
         >>= fun astate ->
         match lhs_access with
         | Base (var, _) when Var.is_return var ->
-            PulseDomain.check_address_of_local_variable summary.Summary.proc_desc rhs_value astate
+            PulseDomain.check_address_of_local_variable summary.Summary.proc_desc rhs_addr astate
         | _ ->
             Ok astate )
     | Closure (pname, captured) ->
@@ -61,7 +63,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
         exec_assign summary lhs_access e loc astate
     | _ ->
         PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate
-        >>= PulseDomain.havoc loc lhs_access
+        >>= PulseDomain.havoc [crumb] loc lhs_access
 
 
   let exec_call summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc
@@ -69,6 +71,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
     let read_all args astate =
       PulseDomain.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
     in
+    let crumb = PulseTrace.Call {f= `HilCall call; actuals; location= call_loc} in
     match call with
     | Direct callee_pname when is_destructor callee_pname -> (
       match actuals with
@@ -86,7 +89,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
       match actuals with
       | AccessExpression constructor_access :: rest ->
           let constructed_object = HilExp.AccessExpression.dereference constructor_access in
-          PulseDomain.havoc call_loc constructed_object astate >>= read_all rest
+          PulseDomain.havoc [crumb] call_loc constructed_object astate >>= read_all rest
       | _ ->
           Ok astate )
     | Direct (Typ.Procname.ObjC_Cpp callee_pname)
@@ -101,7 +104,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
       | [AccessExpression lhs; HilExp.AccessExpression rhs] ->
           let lhs_deref = HilExp.AccessExpression.dereference lhs in
           let rhs_deref = HilExp.AccessExpression.dereference rhs in
-          PulseDomain.havoc call_loc lhs_deref astate
+          PulseDomain.havoc [crumb] call_loc lhs_deref astate
           >>= fun astate -> PulseDomain.read call_loc rhs_deref astate >>| fst
       | _ ->
           read_all actuals astate )
@@ -122,7 +125,9 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
     match model with
     | None ->
         exec_call summary ret call actuals flags call_loc astate
-        >>| PulseDomain.havoc_var (fst ret)
+        >>| PulseDomain.havoc_var
+              [PulseTrace.Call {f= `HilCall call; actuals; location= call_loc}]
+              (fst ret)
     | Some model ->
         model call_loc ~ret ~actuals astate
 
diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml
index 525107979..3ee434b7a 100644
--- a/infer/src/checkers/PulseDomain.ml
+++ b/infer/src/checkers/PulseDomain.ml
@@ -41,6 +41,15 @@ end
 
 (* {3 Heap domain } *)
 
+module AddrTracePair = struct
+  type t = AbstractAddress.t * PulseTrace.t [@@deriving compare]
+
+  let pp f addr_trace =
+    if Config.debug_level_analysis >= 3 then
+      Pp.pair ~fst:AbstractAddress.pp ~snd:PulseTrace.pp f addr_trace
+    else AbstractAddress.pp f (fst addr_trace)
+end
+
 module Attribute = struct
   (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more
        efficient (only need to look at the first element in the set of attributes to know if an
@@ -48,25 +57,18 @@ module Attribute = struct
   type t =
     (* DO NOT MOVE, see toplevel comment *)
     | Invalid of Invalidation.t
-    | AddressOfCppTemporary of Var.t
-    | Closure of
-        Typ.Procname.t
-        * (AccessPath.base * HilExp.AccessExpression.t * AbstractAddress.t) list
-        * Location.t
+    | AddressOfCppTemporary of Var.t * Location.t option
+    | Closure of Typ.Procname.t * AddrTracePair.t list
     | StdVectorReserve
   [@@deriving compare]
 
   let pp f = function
     | Invalid invalidation ->
         Invalidation.pp f invalidation
-    | AddressOfCppTemporary var ->
-        F.fprintf f "&%a" Var.pp var
-    | Closure (pname, captured, location) ->
-        F.fprintf f "%a[%a] (%a)" Typ.Procname.pp pname
-          (Pp.seq ~sep:","
-             (Pp.triple ~fst:AccessPath.pp_base ~snd:HilExp.AccessExpression.pp
-                ~trd:AbstractAddress.pp))
-          captured Location.pp location
+    | AddressOfCppTemporary (var, location_opt) ->
+        F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt
+    | Closure (pname, captured) ->
+        F.fprintf f "%a[%a]" Typ.Procname.pp pname (Pp.seq ~sep:"," AddrTracePair.pp) captured
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
 end
@@ -79,7 +81,7 @@ module Memory : sig
 
   module Edges : PrettyPrintable.PPMap with type key = Access.t
 
-  type edges = AbstractAddress.t Edges.t
+  type edges = AddrTracePair.t Edges.t
 
   type cell = edges * Attributes.t
 
@@ -95,11 +97,11 @@ module Memory : sig
 
   val pp : F.formatter -> t -> unit
 
-  val add_edge : AbstractAddress.t -> Access.t -> AbstractAddress.t -> t -> t
+  val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
 
-  val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AbstractAddress.t -> t -> t
+  val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
 
-  val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AbstractAddress.t option
+  val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option
 
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
 
@@ -120,7 +122,7 @@ end = struct
 
   module Edges = PrettyPrintable.MakePPMap (Access)
 
-  type edges = AbstractAddress.t Edges.t [@@deriving compare]
+  type edges = AddrTracePair.t Edges.t [@@deriving compare]
 
   type cell = edges * Attributes.t [@@deriving compare]
 
@@ -129,33 +131,33 @@ end = struct
   type t = cell Graph.t [@@deriving compare]
 
   let pp =
-    Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AbstractAddress.pp) ~snd:Attributes.pp)
+    Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AddrTracePair.pp) ~snd:Attributes.pp)
 
 
   (* {3 Helper functions to traverse the two maps at once } *)
 
-  let add_edge addr_src access addr_end memory =
+  let add_edge addr_src access value memory =
     let edges, attrs =
       match Graph.find_opt addr_src memory with
-      | Some edges_attrs ->
-          edges_attrs
+      | Some cell ->
+          cell
       | None ->
           (Edges.empty, Attributes.empty)
     in
-    Graph.add addr_src (Edges.add access addr_end edges, attrs) memory
+    Graph.add addr_src (Edges.add access value edges, attrs) memory
 
 
   (** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because
       [*(&x) = &( *x ) = x]. *)
-  let add_edge_and_back_edge addr_src (access : Access.t) addr_end memory =
-    let memory = add_edge addr_src access addr_end memory in
+  let add_edge_and_back_edge addr_src (access : Access.t) addr_trace_dst memory =
+    let memory = add_edge addr_src access addr_trace_dst memory in
     match access with
     | ArrayAccess _ | FieldAccess _ ->
         memory
     | TakeAddress ->
-        add_edge addr_end Dereference addr_src memory
+        add_edge (fst addr_trace_dst) Dereference (addr_src, []) memory
     | Dereference ->
-        add_edge addr_end TakeAddress addr_src memory
+        add_edge (fst addr_trace_dst) TakeAddress (addr_src, []) memory
 
 
   let find_edge_opt addr access memory =
@@ -217,7 +219,7 @@ end = struct
   let fold = Graph.fold
 end
 
-(** Stacks: map addresses of variables to values.
+(** Stacks: map addresses of variables to values and initialisation location.
 
     This is defined as an abstract domain but the domain operations are mostly meaningless on their
     own. It so happens that the join on abstract states uses the join of stacks provided by this
@@ -238,15 +240,15 @@ module Stack = struct
   end
 
   module ValueDomain = struct
-    type t = AbstractAddress.t
+    type t = AbstractAddress.t * Location.t option [@@deriving compare]
 
-    let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs
+    let join ((addr1, _) as v1) ((addr2, _) as v2) = if addr1 <= addr2 then v1 else v2
 
-    let join l1 l2 = min l1 l2
+    let ( <= ) ~lhs:(lhs_addr, _) ~rhs:(rhs_addr, _) = AbstractAddress.equal lhs_addr rhs_addr
 
     let widen ~prev ~next ~num_iters:_ = join prev next
 
-    let pp = AbstractAddress.pp
+    let pp = Pp.pair ~fst:AbstractAddress.pp ~snd:(Pp.option Location.pp)
   end
 
   include AbstractDomain.Map (VarAddress) (ValueDomain)
@@ -258,7 +260,7 @@ module Stack = struct
     PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
 
 
-  let compare = compare AbstractAddress.compare
+  let compare = compare ValueDomain.compare
 end
 
 (** the domain *)
@@ -284,11 +286,11 @@ module Domain : AbstractDomain.S with type t = astate = struct
              (Option.map ~f:fst cell, Option.value_map ~default:Attributes.empty ~f:snd cell)
            in
            Memory.Edges.for_all
-             (fun access_lhs addr_dst ->
+             (fun access_lhs (addr_dst, _) ->
                Option.bind edges_rhs_opt ~f:(fun edges_rhs ->
                    Memory.Edges.find_opt access_lhs edges_rhs )
-               |> Option.map ~f:(AbstractAddress.equal addr_dst)
-               |> Option.value ~default:false )
+               |> Option.exists ~f:(fun (addr_dst_rhs, _) ->
+                      AbstractAddress.equal addr_dst_rhs addr_dst ) )
              edges_lhs
            && Attributes.( <= ) ~lhs:attrs_lhs ~rhs:attrs_rhs )
          lhs.heap
@@ -318,22 +320,23 @@ module Domain : AbstractDomain.S with type t = astate = struct
 
     type nonrec t = {subst: AddressUF.t; astate: t}
 
-    (** adds [(src_addr, access, dst_addr)] to [union_heap] and record potential new equality that
+    (** adds [(src_addr, access, value)] to [union_heap] and record potential new equality that
        results from it in [subst] *)
-    let union_one_edge subst src_addr access dst_addr union_heap =
+    let union_one_edge subst src_addr access value union_heap =
+      let dst_addr, _ = value in
       let src_addr = to_canonical_address subst src_addr in
       let dst_addr = to_canonical_address subst dst_addr in
       match (Memory.find_edge_opt src_addr access union_heap, (access : Memory.Access.t)) with
-      | Some dst_addr', _ when AbstractAddress.equal dst_addr dst_addr' ->
+      | Some (dst_addr', _), _ when AbstractAddress.equal dst_addr dst_addr' ->
           (* same edge *)
           (union_heap, `No_new_equality)
       | _, ArrayAccess _ ->
           (* do not trust array accesses for now, replace the destination of the edge by a fresh location *)
-          ( Memory.add_edge src_addr access (AbstractAddress.mk_fresh ()) union_heap
+          ( Memory.add_edge src_addr access (AbstractAddress.mk_fresh (), []) union_heap
           , `No_new_equality )
       | None, _ ->
-          (Memory.add_edge src_addr access dst_addr union_heap, `No_new_equality)
-      | Some dst_addr', _ ->
+          (Memory.add_edge src_addr access value union_heap, `No_new_equality)
+      | Some (dst_addr', _), _ ->
           (* new equality [dst_addr = dst_addr'] found *)
           ignore (AddressUF.union subst dst_addr dst_addr') ;
           (union_heap, `New_equality)
@@ -345,10 +348,10 @@ module Domain : AbstractDomain.S with type t = astate = struct
       if Addresses.mem addr visited then (visited, union_heap)
       else
         let visited = Addresses.add addr visited in
-        let visit_edge access addr_dst (visited, union_heap) =
-          union_one_edge subst addr access addr_dst union_heap
+        let visit_edge access value (visited, union_heap) =
+          union_one_edge subst addr access value union_heap
           |> fst
-          |> visit_address subst visited heap addr_dst
+          |> visit_address subst visited heap (fst value)
         in
         Memory.find_opt addr heap
         |> Option.fold ~init:(visited, union_heap) ~f:(fun (visited, union_heap) (edges, attrs) ->
@@ -361,7 +364,8 @@ module Domain : AbstractDomain.S with type t = astate = struct
       let visited = Addresses.empty in
       let _, union_heap =
         Stack.fold
-          (fun _var addr (visited, union_heap) -> visit_address subst visited heap addr union_heap)
+          (fun _var (addr, _) (visited, union_heap) ->
+            visit_address subst visited heap addr union_heap )
           stack (visited, union_heap)
       in
       union_heap
@@ -374,7 +378,7 @@ module Domain : AbstractDomain.S with type t = astate = struct
          Stack.merge
            (fun _var addr1_opt addr2_opt ->
              Option.both addr1_opt addr2_opt
-             |> Option.iter ~f:(fun (addr1, addr2) ->
+             |> Option.iter ~f:(fun ((addr1, _), (addr2, _)) ->
                     (* stack1 says [_var = addr1] and stack2 says [_var = addr2]: unify the
                        addresses since they are equal to the same variable *)
                     ignore (AddressUF.union subst addr1 addr2) ) ;
@@ -420,7 +424,11 @@ module Domain : AbstractDomain.S with type t = astate = struct
                 AddressUnionSet.pp set )
         in
         L.d_printfln "Join unified addresses:@\n@[<v2>  %a@]" pp_union_find_classes state.subst ;
-        let stack = Stack.map (to_canonical_address state.subst) state.astate.stack in
+        let stack =
+          Stack.map
+            (fun (addr, loc) -> (to_canonical_address state.subst addr, loc))
+            state.astate.stack
+        in
         {heap; stack} )
       else normalize {state with astate= {state.astate with heap}}
   end
@@ -487,30 +495,12 @@ end
 
 type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare]
 
-type allocator =
-  | Unknown
-  | Closure of
-      { lambda: HilExp.AccessExpression.t  (** some way to refer to the closure *)
-      ; access_expr: HilExp.AccessExpression.t  (** the access expr that was captured *)
-      ; as_base: AccessPath.base  (** the variable it was captured as *)
-      ; location: Location.t }
-
-let pp_allocator f = function
-  | Unknown ->
-      ()
-  | Closure {lambda; access_expr; as_base} ->
-      F.fprintf f "`%a` captured by `%a` as `%a` " HilExp.AccessExpression.pp access_expr
-        HilExp.AccessExpression.pp lambda AccessPath.pp_base as_base
-
-
-let location_of_allocator = function Unknown -> None | Closure {location} -> Some location
-
 module Diagnostic = struct
   type t =
     | AccessToInvalidAddress of
-        { allocated_by: allocator
-        ; invalidated_by: Invalidation.t
+        { invalidated_by: Invalidation.t
         ; accessed_by: actor
+        ; trace: PulseTrace.t
         ; address: AbstractAddress.t }
     | StackVariableAddressEscape of {variable: Var.t; location: Location.t}
 
@@ -520,13 +510,13 @@ module Diagnostic = struct
 
 
   let get_message = function
-    | AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by; address} ->
+    | AccessToInvalidAddress {accessed_by; invalidated_by; address; trace} ->
         let pp_debug_address f =
           if Config.debug_mode then F.fprintf f " (debug: %a)" AbstractAddress.pp address
         in
         F.asprintf "`%a` accesses address %a%a past its lifetime%t" HilExp.AccessExpression.pp
-          accessed_by.access_expr pp_allocator allocated_by Invalidation.pp invalidated_by
-          pp_debug_address
+          accessed_by.access_expr PulseTrace.pp_interesting_events trace Invalidation.pp
+          invalidated_by pp_debug_address
     | StackVariableAddressEscape {variable} ->
         let pp_var f var =
           if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary"
@@ -536,16 +526,7 @@ module Diagnostic = struct
 
 
   let get_trace = function
-    | AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by} ->
-        let allocated_by_trace =
-          match location_of_allocator allocated_by with
-          | None ->
-              []
-          | Some location ->
-              [ Errlog.make_trace_element 0 location
-                  (F.asprintf "%ahere" pp_allocator allocated_by)
-                  [] ]
-        in
+    | AccessToInvalidAddress {accessed_by; invalidated_by; trace} ->
         let invalidated_by_trace =
           Invalidation.get_location invalidated_by
           |> Option.map ~f:(fun location ->
@@ -554,7 +535,8 @@ module Diagnostic = struct
                    [] )
           |> Option.to_list
         in
-        allocated_by_trace @ invalidated_by_trace
+        PulseTrace.make_errlog_trace ~depth:0 trace
+        @ invalidated_by_trace
         @ [ Errlog.make_trace_element 0 accessed_by.location
               (F.asprintf "accessed `%a` here" HilExp.AccessExpression.pp accessed_by.access_expr)
               [] ]
@@ -576,12 +558,11 @@ module Operations = struct
   open Result.Monad_infix
 
   (** Check that the address is not known to be invalid *)
-  let check_addr_access ?(allocated_by = Unknown) actor address astate =
+  let check_addr_access actor (address, trace) astate =
     match Memory.get_invalidation address astate.heap with
     | Some invalidated_by ->
         Error
-          (Diagnostic.AccessToInvalidAddress
-             {invalidated_by; accessed_by= actor; address; allocated_by})
+          (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address; trace})
     | None ->
         Ok astate
 
@@ -590,52 +571,55 @@ module Operations = struct
    and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it
    is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each
    address reached is valid. *)
-  let rec walk ~dereference_to_ignore actor ~on_last addr path astate =
-    let check_addr_access_optional actor addr astate =
+  let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate =
+    let check_addr_access_optional actor addr_trace astate =
       match dereference_to_ignore with
       | Some 0 ->
           Ok astate
       | _ ->
-          check_addr_access actor addr astate
+          check_addr_access actor addr_trace astate
     in
     match (path, on_last) with
     | [], `Access ->
-        Ok (astate, addr)
+        Ok (astate, addr_trace)
     | [], `Overwrite _ ->
         L.die InternalError "Cannot overwrite last address in empty path"
-    | [a], `Overwrite new_addr ->
-        check_addr_access_optional actor addr astate
+    | [a], `Overwrite new_addr_trace ->
+        check_addr_access_optional actor addr_trace astate
         >>| fun astate ->
-        let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in
-        ({astate with heap}, new_addr)
+        let heap = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate.heap in
+        ({astate with heap}, new_addr_trace)
     | a :: path, _ -> (
-        check_addr_access_optional actor addr astate
+        check_addr_access_optional actor addr_trace astate
         >>= fun astate ->
         let dereference_to_ignore =
           Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore
         in
+        let addr = fst addr_trace in
         match Memory.find_edge_opt addr a astate.heap with
         | None ->
-            let addr' = AbstractAddress.mk_fresh () in
-            let heap = Memory.add_edge_and_back_edge addr a addr' astate.heap in
+            let addr_trace' = (AbstractAddress.mk_fresh (), []) in
+            let heap = Memory.add_edge_and_back_edge addr a addr_trace' astate.heap in
             let astate = {astate with heap} in
-            walk ~dereference_to_ignore actor ~on_last addr' path astate
-        | Some addr' ->
-            walk ~dereference_to_ignore actor ~on_last addr' path astate )
+            walk ~dereference_to_ignore actor ~on_last addr_trace' path astate
+        | Some addr_trace' ->
+            walk ~dereference_to_ignore actor ~on_last addr_trace' path astate )
 
 
-  let write_var var new_addr astate =
+  let write_var var new_addr_trace astate =
     let astate, var_address_of =
       match Stack.find_opt var astate.stack with
-      | Some addr ->
+      | Some (addr, _) ->
           (astate, addr)
       | None ->
           let addr = AbstractAddress.mk_fresh () in
-          let stack = Stack.add var addr astate.stack in
+          let stack = Stack.add var (addr, None) astate.stack in
           ({astate with stack}, addr)
     in
     (* Update heap with var_address_of -*-> new_addr *)
-    let heap = Memory.add_edge var_address_of HilExp.Access.Dereference new_addr astate.heap in
+    let heap =
+      Memory.add_edge var_address_of HilExp.Access.Dereference new_addr_trace astate.heap
+    in
     {astate with heap}
 
 
@@ -672,7 +656,7 @@ module Operations = struct
     with Failed_fold diag -> Error diag
 
 
-  (** add addresses to the state to give a address to the destination of the given access path *)
+  (** add addresses to the state to give an address to the destination of the given access path *)
   and walk_access_expr ~on_last astate access_expr location =
     to_accesses location access_expr astate
     >>= fun (astate, (access_var, _), access_list) ->
@@ -684,24 +668,28 @@ module Operations = struct
         (Pp.seq ~sep:"," Memory.Access.pp)
         access_list ;
     match (on_last, access_list) with
-    | `Overwrite new_addr, [] ->
-        Ok (write_var access_var new_addr astate, new_addr)
+    | `Overwrite new_addr_trace, [] ->
+        Ok (write_var access_var new_addr_trace astate, new_addr_trace)
     | `Access, _ | `Overwrite _, _ :: _ -> (
-        let astate, base_addr =
+        let astate, base_addr_trace =
           match Stack.find_opt access_var astate.stack with
-          | Some addr ->
-              (astate, addr)
+          | Some (addr, init_loc_opt) ->
+              let trace =
+                Option.value_map init_loc_opt ~default:[] ~f:(fun init_loc ->
+                    [PulseTrace.VariableDeclaration init_loc] )
+              in
+              (astate, (addr, trace))
           | None ->
               let addr = AbstractAddress.mk_fresh () in
-              let stack = Stack.add access_var addr astate.stack in
-              ({astate with stack}, addr)
+              let stack = Stack.add access_var (addr, None) astate.stack in
+              ({astate with stack}, (addr, []))
         in
         match access_list with
         | [HilExp.Access.TakeAddress] ->
-            Ok (astate, base_addr)
+            Ok (astate, base_addr_trace)
         | _ ->
             let actor = {access_expr; location} in
-            walk ~dereference_to_ignore actor ~on_last base_addr
+            walk ~dereference_to_ignore actor ~on_last base_addr_trace
               (HilExp.Access.Dereference :: access_list)
               astate )
 
@@ -715,9 +703,9 @@ module Operations = struct
 
   and read location access_expr astate =
     materialize_address astate access_expr location
-    >>= fun (astate, addr) ->
+    >>= fun (astate, addr_trace) ->
     let actor = {access_expr; location} in
-    check_addr_access actor addr astate >>| fun astate -> (astate, addr)
+    check_addr_access actor addr_trace astate >>| fun astate -> (astate, addr_trace)
 
 
   and read_all location access_exprs astate =
@@ -728,7 +716,7 @@ module Operations = struct
   and eval_hil_exp location (hil_exp : HilExp.t) astate =
     match hil_exp with
     | AccessExpression access_expr ->
-        read location access_expr astate
+        read location access_expr astate >>| fun (astate, (addr, _)) -> (astate, addr)
     | _ ->
         read_all location (HilExp.get_access_exprs hil_exp) astate
         >>| fun astate -> (astate, AbstractAddress.mk_fresh ())
@@ -739,8 +727,8 @@ module Operations = struct
     address.
 
     Return an error state if it traverses some known invalid address. *)
-  let overwrite_address astate access_expr new_addr =
-    walk_access_expr ~on_last:(`Overwrite new_addr) astate access_expr
+  let overwrite_address astate access_expr new_addr_trace =
+    walk_access_expr ~on_last:(`Overwrite new_addr_trace) astate access_expr
 
 
   (** Add the given address to the set of know invalid addresses. *)
@@ -748,10 +736,10 @@ module Operations = struct
     {astate with heap= Memory.invalidate address actor astate.heap}
 
 
-  let havoc_var var astate = write_var var (AbstractAddress.mk_fresh ()) astate
+  let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate
 
-  let havoc location (access_expr : HilExp.AccessExpression.t) astate =
-    overwrite_address astate access_expr (AbstractAddress.mk_fresh ()) location >>| fst
+  let havoc trace location (access_expr : HilExp.AccessExpression.t) astate =
+    overwrite_address astate access_expr (AbstractAddress.mk_fresh (), trace) location >>| fst
 
 
   let write location access_expr addr astate =
@@ -760,21 +748,22 @@ module Operations = struct
 
   let invalidate cause location access_expr astate =
     materialize_address astate access_expr location
-    >>= fun (astate, addr) ->
-    check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr
+    >>= fun (astate, addr_trace) ->
+    check_addr_access {access_expr; location} addr_trace astate
+    >>| mark_invalid cause (fst addr_trace)
 
 
   let invalidate_array_elements cause location access_expr astate =
     materialize_address astate access_expr location
-    >>= fun (astate, addr) ->
-    check_addr_access {access_expr; location} addr astate
+    >>= fun (astate, addr_trace) ->
+    check_addr_access {access_expr; location} addr_trace astate
     >>| fun astate ->
-    match Memory.find_opt addr astate.heap with
+    match Memory.find_opt (fst addr_trace) astate.heap with
     | None ->
         astate
     | Some (edges, _) ->
         Memory.Edges.fold
-          (fun access dest_addr astate ->
+          (fun access (dest_addr, _) astate ->
             match (access : Memory.Access.t) with
             | ArrayAccess _ ->
                 mark_invalid cause dest_addr astate
@@ -792,62 +781,74 @@ module Operations = struct
              Container.fold_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
                attrs ~init:() ~f:(fun () attr ->
                  match attr with
-                 | Attribute.AddressOfCppTemporary variable ->
-                     Error
-                       (Diagnostic.StackVariableAddressEscape {variable; location= proc_location})
+                 | Attribute.AddressOfCppTemporary (variable, location_opt) ->
+                     let location = Option.value ~default:proc_location location_opt in
+                     Error (Diagnostic.StackVariableAddressEscape {variable; location})
                  | _ ->
                      Ok () ) )
     in
     let check_address_of_stack_variable () =
       Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold)
-        astate.stack ~init:() ~f:(fun () (variable, var_address) ->
+        astate.stack ~init:() ~f:(fun () (variable, (var_address, init_location)) ->
           if
             AbstractAddress.equal var_address address
             && ( Var.is_cpp_temporary variable
                || Var.is_local_to_procedure proc_name variable
                   && not (Procdesc.is_captured_var proc_desc variable) )
-          then Error (Diagnostic.StackVariableAddressEscape {variable; location= proc_location})
+          then
+            let location = Option.value ~default:proc_location init_location in
+            Error (Diagnostic.StackVariableAddressEscape {variable; location})
           else Ok () )
     in
     check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate
 
 
-  let mark_address_of_cpp_temporary variable address heap =
-    Memory.add_attributes address (Attributes.singleton (AddressOfCppTemporary variable)) heap
+  let mark_address_of_cpp_temporary location variable address heap =
+    Memory.add_attributes address
+      (Attributes.singleton (AddressOfCppTemporary (variable, location)))
+      heap
 
 
   let remove_vars vars astate =
     let heap =
       List.fold vars ~init:astate.heap ~f:(fun heap var ->
           match Stack.find_opt var astate.stack with
-          | Some address when Var.is_cpp_temporary var ->
+          | Some (address, location) when Var.is_cpp_temporary var ->
               (* TODO: it would be good to record the location of the temporary creation in the
                  stack and save it here in the attribute for reporting *)
-              mark_address_of_cpp_temporary var address heap
+              mark_address_of_cpp_temporary location var address heap
           | _ ->
               heap )
     in
     let stack = List.fold ~f:(fun stack var -> Stack.remove var stack) ~init:astate.stack vars in
     if phys_equal stack astate.stack && phys_equal heap astate.heap then astate else {stack; heap}
+
+
+  let record_var_decl_location location var astate =
+    let addr =
+      match Stack.find_opt var astate.stack with
+      | Some (addr, _) ->
+          addr
+      | None ->
+          AbstractAddress.mk_fresh ()
+    in
+    let stack = Stack.add var (addr, Some location) astate.stack in
+    {astate with stack}
 end
 
 module Closures = struct
   open Result.Monad_infix
 
-  let check_captured_addresses location lambda address astate =
-    match Memory.find_opt address astate.heap with
+  let check_captured_addresses location lambda addr astate =
+    match Memory.find_opt addr astate.heap with
     | None ->
         Ok astate
     | Some (_, attributes) ->
         IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
           attributes ~f:(function
-          | Attribute.Closure (_, captured, lambda_location) ->
-              IContainer.iter_result ~fold:List.fold captured
-                ~f:(fun (base, access_expr, address) ->
-                  Operations.check_addr_access
-                    ~allocated_by:
-                      (Closure {lambda; access_expr; as_base= base; location= lambda_location})
-                    {access_expr= lambda; location} address astate
+          | Attribute.Closure (_, captured) ->
+              IContainer.iter_result ~fold:List.fold captured ~f:(fun addr_trace ->
+                  Operations.check_addr_access {access_expr= lambda; location} addr_trace astate
                   >>| fun _ -> () )
           | _ ->
               Ok () )
@@ -856,23 +857,28 @@ module Closures = struct
 
   let write location access_expr pname captured astate =
     let closure_addr = AbstractAddress.mk_fresh () in
-    Operations.write location access_expr closure_addr astate
+    Operations.write location access_expr
+      (closure_addr, [PulseTrace.Assignment {lhs= access_expr; location}])
+      astate
     >>| fun astate ->
     { astate with
       heap=
         Memory.add_attributes closure_addr
-          (Attributes.singleton (Closure (pname, captured, location)))
+          (Attributes.singleton (Closure (pname, captured)))
           astate.heap }
 
 
   let record location access_expr pname captured astate =
     List.fold_result captured ~init:(astate, [])
-      ~f:(fun ((astate, captured) as result) (captured_base, captured_exp) ->
+      ~f:(fun ((astate, captured) as result) (captured_as, captured_exp) ->
         match captured_exp with
-        | HilExp.AccessExpression (AddressOf access_expr) ->
+        | HilExp.AccessExpression (AddressOf access_expr as captured_access_expr) ->
             Operations.read location access_expr astate
-            >>= fun (astate, address) ->
-            Ok (astate, (captured_base, access_expr, address) :: captured)
+            >>= fun (astate, (address, trace)) ->
+            let new_trace =
+              PulseTrace.Capture {captured_as; captured= captured_access_expr; location} :: trace
+            in
+            Ok (astate, (address, new_trace) :: captured)
         | _ ->
             Ok result )
     >>= fun (astate, captured_addresses) ->
@@ -884,12 +890,12 @@ module StdVector = struct
 
   let is_reserved location vector_access_expr astate =
     Operations.read location vector_access_expr astate
-    >>| fun (astate, addr) -> (astate, Memory.is_std_vector_reserved addr astate.heap)
+    >>| fun (astate, (addr, _)) -> (astate, Memory.is_std_vector_reserved addr astate.heap)
 
 
   let mark_reserved location vector_access_expr astate =
     Operations.read location vector_access_expr astate
-    >>| fun (astate, addr) -> {astate with heap= Memory.std_vector_reserve addr astate.heap}
+    >>| fun (astate, (addr, _)) -> {astate with heap= Memory.std_vector_reserve addr astate.heap}
 end
 
 include Domain
diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli
index acca1965e..7235f9ca1 100644
--- a/infer/src/checkers/PulseDomain.mli
+++ b/infer/src/checkers/PulseDomain.mli
@@ -54,17 +54,26 @@ module StdVector : sig
   val mark_reserved : Location.t -> HilExp.AccessExpression.t -> t -> t access_result
 end
 
-val read : Location.t -> HilExp.AccessExpression.t -> t -> (t * AbstractAddress.t) access_result
+val read :
+     Location.t
+  -> HilExp.AccessExpression.t
+  -> t
+  -> (t * (AbstractAddress.t * PulseTrace.t)) access_result
 
 val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result
 
-val havoc_var : Var.t -> t -> t
+val havoc_var : PulseTrace.t -> Var.t -> t -> t
 
-val havoc : Location.t -> HilExp.AccessExpression.t -> t -> t access_result
+val havoc : PulseTrace.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
 
-val write_var : Var.t -> AbstractAddress.t -> t -> t
+val write_var : Var.t -> AbstractAddress.t * PulseTrace.t -> t -> t
 
-val write : Location.t -> HilExp.AccessExpression.t -> AbstractAddress.t -> t -> t access_result
+val write :
+     Location.t
+  -> HilExp.AccessExpression.t
+  -> AbstractAddress.t * PulseTrace.t
+  -> t
+  -> t access_result
 
 val invalidate :
   PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
@@ -72,6 +81,9 @@ val invalidate :
 val invalidate_array_elements :
   PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
 
+val record_var_decl_location : Location.t -> Var.t -> t -> t
+
 val remove_vars : Var.t list -> t -> t
 
+(* TODO: better name and pass location to report where we returned *)
 val check_address_of_local_variable : Procdesc.t -> AbstractAddress.t -> t -> t access_result
diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml
index 0759cb67a..56e7e3c5b 100644
--- a/infer/src/checkers/PulseInvalidation.ml
+++ b/infer/src/checkers/PulseInvalidation.ml
@@ -18,7 +18,7 @@ type std_vector_function =
   | ShrinkToFit
 [@@deriving compare]
 
-let std_vector_function_pp f = function
+let pp_std_vector_function f = function
   | Assign ->
       F.fprintf f "std::vector::assign"
   | Clear ->
@@ -71,15 +71,15 @@ let get_location = function
 let pp f = function
   | CFree (access_expr, location) ->
       F.fprintf f "invalidated by call to `free(%a)` at %a" HilExp.AccessExpression.pp access_expr
-        Location.pp location
+        Location.pp_line location
   | CppDelete (access_expr, location) ->
       F.fprintf f "invalidated by call to `delete %a` at %a" HilExp.AccessExpression.pp access_expr
-        Location.pp location
+        Location.pp_line location
   | CppDestructor (proc_name, access_expr, location) ->
       F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name
-        HilExp.AccessExpression.pp access_expr Location.pp location
+        HilExp.AccessExpression.pp access_expr Location.pp_line location
   | Nullptr ->
       F.fprintf f "null pointer"
   | StdVector (std_vector_f, access_expr, location) ->
-      F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" std_vector_function_pp
-        std_vector_f HilExp.AccessExpression.pp access_expr Location.pp location
+      F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" pp_std_vector_function
+        std_vector_f HilExp.AccessExpression.pp access_expr Location.pp_line location
diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli
index 65235de51..252ea3a28 100644
--- a/infer/src/checkers/PulseInvalidation.mli
+++ b/infer/src/checkers/PulseInvalidation.mli
@@ -17,6 +17,8 @@ type std_vector_function =
   | ShrinkToFit
 [@@deriving compare]
 
+val pp_std_vector_function : Format.formatter -> std_vector_function -> unit
+
 type t =
   | CFree of HilExp.AccessExpression.t * Location.t
   | CppDelete of HilExp.AccessExpression.t * Location.t
diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml
index 770d9208c..1cb10542e 100644
--- a/infer/src/checkers/PulseModels.ml
+++ b/infer/src/checkers/PulseModels.ml
@@ -34,8 +34,10 @@ module C = struct
   let variable_initialization : model =
    fun location ~ret:_ ~actuals astate ->
     match actuals with
-    | [AccessExpression (AddressOf access_expr)] ->
-        PulseDomain.havoc location access_expr astate
+    | [AccessExpression (AddressOf (Base (var, _)))] ->
+        PulseDomain.havoc_var [PulseTrace.VariableDeclaration location] var astate
+        |> PulseDomain.record_var_decl_location location var
+        |> Result.return
     | _ ->
         L.die InternalError
           "The frontend is not supposed to produce __variable_initialization(e) where e is not of \
@@ -65,10 +67,10 @@ module Cplusplus = struct
     | AccessExpression lambda :: _ ->
         PulseDomain.read location HilExp.AccessExpression.(dereference lambda) astate
         >>= fun (astate, address) ->
-        PulseDomain.Closures.check_captured_addresses location lambda address astate
+        PulseDomain.Closures.check_captured_addresses location lambda (fst address) astate
     | _ ->
         Ok astate )
-    >>| PulseDomain.havoc_var ret_var
+    >>| PulseDomain.havoc_var [PulseTrace.Call {f= `Model "<lambda>"; actuals; location}] ret_var
 
 
   let placement_new : model =
@@ -76,15 +78,16 @@ module Cplusplus = struct
     let read_all args astate =
       PulseDomain.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate
     in
+    let crumb = PulseTrace.Call {f= `Model "<placement new>"; actuals; location} in
     match List.rev actuals with
     | HilExp.AccessExpression expr :: other_actuals ->
         PulseDomain.read location expr astate
-        >>= fun (astate, address) ->
-        Ok (PulseDomain.write_var ret_var address astate) >>= read_all other_actuals
+        >>= fun (astate, (address, trace)) ->
+        PulseDomain.write_var ret_var (address, crumb :: trace) astate |> read_all other_actuals
     | _ :: other_actuals ->
-        read_all other_actuals astate >>| PulseDomain.havoc_var ret_var
+        read_all other_actuals astate >>| PulseDomain.havoc_var [crumb] ret_var
     | _ ->
-        Ok (PulseDomain.havoc_var ret_var astate)
+        Ok (PulseDomain.havoc_var [crumb] ret_var astate)
 end
 
 module StdVector = struct
@@ -104,42 +107,50 @@ module StdVector = struct
     HilExp.AccessExpression.array_offset (deref_internal_array vector) Typ.void index
 
 
-  let reallocate_internal_array vector vector_f location astate =
+  let reallocate_internal_array trace vector vector_f location astate =
     let array_address = to_internal_array vector in
     let array = deref_internal_array vector in
     let invalidation = PulseInvalidation.StdVector (vector_f, vector, location) in
     PulseDomain.invalidate_array_elements invalidation location array astate
     >>= PulseDomain.invalidate invalidation location array
-    >>= PulseDomain.havoc location array_address
+    >>= PulseDomain.havoc trace location array_address
 
 
-  let invalidate_references invalidation : model =
+  let invalidate_references vector_f : model =
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | AccessExpression vector :: _ ->
-        reallocate_internal_array vector invalidation location astate
+        let crumb =
+          PulseTrace.Call
+            { f= `Model (Format.asprintf "%a" PulseInvalidation.pp_std_vector_function vector_f)
+            ; actuals
+            ; location }
+        in
+        reallocate_internal_array [crumb] vector vector_f location astate
     | _ ->
         Ok astate
 
 
   let at : model =
    fun location ~ret ~actuals astate ->
+    let crumb = PulseTrace.Call {f= `Model "std::vector::at"; actuals; location} in
     match actuals with
     | [AccessExpression vector_access_expr; index_exp] ->
         PulseDomain.read location
           (element_of_internal_array vector_access_expr (Some index_exp))
           astate
-        >>= fun (astate, loc) ->
-        PulseDomain.write location (HilExp.AccessExpression.base ret) loc astate
+        >>= fun (astate, (addr, trace)) ->
+        PulseDomain.write location (HilExp.AccessExpression.base ret) (addr, crumb :: trace) astate
     | _ ->
-        Ok (PulseDomain.havoc_var (fst ret) astate)
+        Ok (PulseDomain.havoc_var [crumb] (fst ret) astate)
 
 
   let reserve : model =
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        reallocate_internal_array vector Reserve location astate
+        let crumb = PulseTrace.Call {f= `Model "std::vector::reserve"; actuals; location} in
+        reallocate_internal_array [crumb] vector Reserve location astate
         >>= PulseDomain.StdVector.mark_reserved location vector
     | _ ->
         Ok astate
@@ -149,6 +160,7 @@ module StdVector = struct
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
+        let crumb = PulseTrace.Call {f= `Model "std::vector::push_back"; actuals; location} in
         PulseDomain.StdVector.is_reserved location vector astate
         >>= fun (astate, is_reserved) ->
         if is_reserved then
@@ -157,7 +169,7 @@ module StdVector = struct
           Ok astate
         else
           (* simulate a re-allocation of the underlying array every time an element is added *)
-          reallocate_internal_array vector PushBack location astate
+          reallocate_internal_array [crumb] vector PushBack location astate
     | _ ->
         Ok astate
 end
diff --git a/infer/src/checkers/PulseTrace.ml b/infer/src/checkers/PulseTrace.ml
new file mode 100644
index 000000000..5013b4c31
--- /dev/null
+++ b/infer/src/checkers/PulseTrace.ml
@@ -0,0 +1,72 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+
+type breadcrumb =
+  | VariableDeclaration of Location.t
+  | Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
+  | Capture of
+      { captured_as: AccessPath.base
+      ; captured: HilExp.AccessExpression.t
+      ; location: Location.t }
+  | Call of
+      { f: [`HilCall of HilInstr.call | `Model of string]
+      ; actuals: HilExp.t list
+      ; location: Location.t }
+[@@deriving compare]
+
+let pp_breadcrumb_no_location fmt = function
+  | VariableDeclaration _ ->
+      F.fprintf fmt "variable declared"
+  | Capture {captured_as; captured; location= _} ->
+      F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured AccessPath.pp_base
+        captured_as
+  | Assignment {lhs; location= _} ->
+      F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
+  | Call {f; actuals; location= _} ->
+      let pp_f fmt = function
+        | `HilCall call ->
+            F.fprintf fmt "%a" HilInstr.pp_call call
+        | `Model model ->
+            F.pp_print_string fmt model
+      in
+      F.fprintf fmt "returned from call to `%a(%a)`" pp_f f (Pp.seq ~sep:"," HilExp.pp) actuals
+
+
+let location_of_breadcrumb = function
+  | VariableDeclaration location | Assignment {location} | Capture {location} | Call {location} ->
+      location
+
+
+let pp_breadcrumb fmt crumb =
+  F.fprintf fmt "%a at %a" pp_breadcrumb_no_location crumb Location.pp_line
+    (location_of_breadcrumb crumb)
+
+
+let errlog_trace_elem_of_breadcrumb ~depth crumb =
+  let location = location_of_breadcrumb crumb in
+  let description = F.asprintf "%a" pp_breadcrumb_no_location crumb in
+  let tags = [] in
+  Errlog.make_trace_element depth location description tags
+
+
+type t = breadcrumb list [@@deriving compare]
+
+let pp f trace = Pp.seq ~print_env:Pp.text_break pp_breadcrumb f trace
+
+let make_errlog_trace ~depth trace = List.rev_map ~f:(errlog_trace_elem_of_breadcrumb ~depth) trace
+
+let pp_last_event f = function
+  | [] ->
+      ()
+  | crumb :: _ ->
+      pp_breadcrumb f crumb ;
+      (* HACK: needed by the call site *) F.pp_print_string f " "
+
+
+let pp_interesting_events f trace = pp_last_event f trace
diff --git a/infer/src/checkers/PulseTrace.mli b/infer/src/checkers/PulseTrace.mli
new file mode 100644
index 000000000..424a64e34
--- /dev/null
+++ b/infer/src/checkers/PulseTrace.mli
@@ -0,0 +1,28 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type breadcrumb =
+  | VariableDeclaration of Location.t
+  | Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
+  | Capture of
+      { captured_as: AccessPath.base
+      ; captured: HilExp.AccessExpression.t
+      ; location: Location.t }
+  | Call of
+      { f: [`HilCall of HilInstr.call | `Model of string]
+      ; actuals: HilExp.t list
+      ; location: Location.t }
+
+type t = breadcrumb list [@@deriving compare]
+
+val pp : Format.formatter -> t -> unit
+
+val make_errlog_trace : depth:int -> t -> Errlog.loc_trace
+
+val pp_interesting_events : Format.formatter -> t -> unit
diff --git a/infer/src/istd/Pp.ml b/infer/src/istd/Pp.ml
index 00edc6f0d..762306cfe 100644
--- a/infer/src/istd/Pp.ml
+++ b/infer/src/istd/Pp.ml
@@ -171,5 +171,3 @@ let cli_args fmt args =
 
 
 let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b
-
-let triple ~fst ~snd ~trd fmt (a, b, c) = F.fprintf fmt "(%a,@,%a@,%a)" fst a snd b trd c
diff --git a/infer/src/istd/Pp.mli b/infer/src/istd/Pp.mli
index 2a80f4421..5b8edcf99 100644
--- a/infer/src/istd/Pp.mli
+++ b/infer/src/istd/Pp.mli
@@ -100,11 +100,3 @@ val pair :
   -> F.formatter
   -> 'a * 'b
   -> unit
-
-val triple :
-     fst:(F.formatter -> 'a -> unit)
-  -> snd:(F.formatter -> 'b -> unit)
-  -> trd:(F.formatter -> 'c -> unit)
-  -> F.formatter
-  -> 'a * 'b * 'c
-  -> unit
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 714c32dc5..33601178e 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,35 +1,35 @@
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `ptr` here]
-codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 29, column 3 here,accessed `&(f)` here]
-codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 20, column 3 here,accessed `&(f)` here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 25, column 5 here,accessed `*(result)` here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here]
+codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$12))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 29 here,accessed `&(f)` here]
+codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 20 here,accessed `&(f)` here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 25 here,accessed `*(result)` here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 37, column 3 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 148, column 3 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 156, column 3 here,accessed `alias` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 165, column 3 here,accessed `alias` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 71, column 3 here,accessed `*(s.f)` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::C_~C(c)` at line 210, column 3 here,accessed `pc->f` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15, column 3 here,accessed `x` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 64, column 5 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 126, column 5 here,accessed `&(this->x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::assign(vec, ..)` at line 83, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::clear(vec, ..)` at line 77, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::insert(vec, ..)` at line 95, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 71, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 89, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 57 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 82 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 18 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 50 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 37 here,accessed `s->f` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 24 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 73 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 102 here,accessed `s->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S_S(&(s),1)`,invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalidated by call to `delete alias` at line 148 here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalidated by call to `delete s` at line 156 here,accessed `alias` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalidated by call to `delete s` at line 165 here,accessed `alias` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S_S(&(s),1)`,invalidated by destructor call `use_after_destructor::S_~S(s)` at line 71 here,accessed `*(s.f)` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::C_C(&(c),3)`,invalidated by destructor call `use_after_destructor::C_~C(c)` at line 210 here,accessed `pc->f` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15 here,accessed `x` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10 here,accessed `*(x)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 65 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 127 here,accessed `&(this->x)` here]
+codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 84 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 78 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 20 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 13 here,accessed `*(y)` here]
+codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 96 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 72 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 90 here,accessed `*(elt)` here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
index 7f082884d..1e666220b 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
@@ -9,8 +9,9 @@
 
 void deref_vector_element_after_push_back_bad(std::vector<int>& vec) {
   int* elt = &vec[1];
+  int* y = elt;
   vec.push_back(42);
-  std::cout << *elt << "\n";
+  std::cout << *y << "\n";
 }
 
 void deref_local_vector_element_after_push_back_bad() {