diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml
index a550a8b57..ab262542c 100644
--- a/infer/src/checkers/impurityDomain.ml
+++ b/infer/src/checkers/impurityDomain.ml
@@ -9,7 +9,7 @@ open! IStd
 module F = Format
 
 type trace =
-  | WrittenTo of unit PulseDomain.InterprocAction.t
+  | WrittenTo of unit PulseDomain.Trace.t
   | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t
 [@@deriving compare]
 
@@ -53,31 +53,19 @@ let pp_param_source fmt = function
 
 
 let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog =
-  let rec aux ~nesting rev_errlog action =
-    match action with
-    | WrittenTo (PulseDomain.InterprocAction.Immediate {location}) ->
-        let rev_errlog =
-          Errlog.make_trace_element nesting location
-            (F.asprintf "%a '%a' is modified at %a" pp_param_source param_source Var.pp var
-               Location.pp location)
-            []
-          :: rev_errlog
-        in
-        List.rev_append rev_errlog errlog
-    | WrittenTo (PulseDomain.InterprocAction.ViaCall {action; f; location}) ->
-        aux ~nesting:(nesting + 1)
-          ( Errlog.make_trace_element nesting location
-              (F.asprintf "%a '%a' is modified when calling %a at %a" pp_param_source param_source
-                 Var.pp var PulseDomain.CallEvent.describe f Location.pp location)
-              []
-          :: rev_errlog )
-          (WrittenTo action)
-    | Invalid trace ->
-        PulseDomain.Trace.add_to_errlog
-          ~header:(F.asprintf "%a '%a'" pp_param_source param_source Var.pp var)
-          (fun f invalidation ->
-            F.fprintf f "%a here" PulseDomain.Invalidation.describe invalidation )
-          trace rev_errlog
+  let aux ~nesting errlog trace =
+    match trace with
+    | WrittenTo access_trace ->
+        PulseDomain.Trace.add_to_errlog ~nesting
+          (fun fmt () ->
+            F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
+          access_trace errlog
+    | Invalid invalidation_trace ->
+        PulseDomain.Trace.add_to_errlog ~nesting
+          (fun fmt invalid ->
+            F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
+              PulseDomain.Invalidation.describe invalid )
+          invalidation_trace errlog
   in
   let first_trace, rest = trace_list in
-  List.fold_left rest ~init:(aux ~nesting [] first_trace) ~f:(aux ~nesting)
+  List.fold_left rest ~init:(aux ~nesting errlog first_trace) ~f:(aux ~nesting)
diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli
index 9babc56b0..349b4a920 100644
--- a/infer/src/checkers/impurityDomain.mli
+++ b/infer/src/checkers/impurityDomain.mli
@@ -7,9 +7,8 @@
 open! IStd
 
 type trace =
-  | WrittenTo of unit PulseDomain.InterprocAction.t
+  | WrittenTo of unit PulseDomain.Trace.t
   | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t
-[@@deriving compare]
 
 module ModifiedVar : sig
   type nonempty_action_type = trace * trace list
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index a7902e860..9e6dc096f 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -9,7 +9,6 @@ module F = Format
 module L = Logging
 open Result.Monad_infix
 module AbstractAddress = PulseDomain.AbstractAddress
-module InterprocAction = PulseDomain.InterprocAction
 module Invalidation = PulseDomain.Invalidation
 module ValueHistory = PulseDomain.ValueHistory
 
@@ -55,7 +54,7 @@ module PulseTransferFunctions = struct
   type extras = unit
 
   let exec_unknown_call reason ret call actuals _flags call_loc astate =
-    let event = ValueHistory.Call {f= reason; location= call_loc} in
+    let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in
     let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in
     match proc_name_of_call call with
     | Some callee_pname when Typ.Procname.is_constructor callee_pname -> (
@@ -105,14 +104,12 @@ module PulseTransferFunctions = struct
 
   (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *)
   let exec_object_out_of_scope call_loc (pvar, typ) astate =
-    let event =
-      InterprocAction.Immediate {imm= Invalidation.GoneOutOfScope (pvar, typ); location= call_loc}
-    in
+    let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
     (* invalidate both [&x] and [x]: reading either is now forbidden *)
     PulseOperations.eval call_loc (Exp.Lvar pvar) astate
     >>= fun (astate, out_of_scope_base) ->
-    PulseOperations.invalidate_deref call_loc event out_of_scope_base astate
-    >>= PulseOperations.invalidate call_loc event out_of_scope_base
+    PulseOperations.invalidate_deref call_loc gone_out_of_scope out_of_scope_base astate
+    >>= PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base
 
 
   let dispatch_call summary ret call_exp actuals call_loc flags astate =
@@ -161,8 +158,7 @@ module PulseTransferFunctions = struct
         (* [lhs_id := *rhs_exp] *)
         let result =
           PulseOperations.eval_deref loc rhs_exp astate
-          >>| fun (astate, (rhs_addr, rhs_history)) ->
-          PulseOperations.write_id lhs_id (rhs_addr, rhs_history) astate
+          >>| fun (astate, rhs_addr_hist) -> PulseOperations.write_id lhs_id rhs_addr_hist astate
         in
         [check_error summary result]
     | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index fff5cdc70..494bd89fb 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -10,6 +10,9 @@ module L = Logging
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
 module Attributes = PulseDomain.Attributes
+module Invalidation = PulseDomain.Invalidation
+module Trace = PulseDomain.Trace
+module ValueHistory = PulseDomain.ValueHistory
 module BaseStack = PulseDomain.Stack
 module BaseMemory = PulseDomain.Memory
 
@@ -98,21 +101,21 @@ module Stack = struct
     if phys_equal new_post astate.post then astate else {astate with post= new_post}
 
 
-  let eval var astate =
+  let eval origin var astate =
     match BaseStack.find_opt var (astate.post :> base_domain).stack with
     | Some addr_hist ->
         (astate, addr_hist)
     | None ->
-        let addr_hist = (AbstractAddress.mk_fresh (), []) in
+        let addr = AbstractAddress.mk_fresh () in
+        let addr_hist = (addr, origin) in
         let post_stack = BaseStack.add var addr_hist (astate.post :> base_domain).stack in
         let pre =
           (* do not overwrite values of variables already in the pre *)
           if (not (BaseStack.mem var (astate.pre :> base_domain).stack)) && is_abducible astate var
           then
-            let foot_stack = BaseStack.add var addr_hist (astate.pre :> base_domain).stack in
-            let foot_heap =
-              BaseMemory.register_address (fst addr_hist) (astate.pre :> base_domain).heap
-            in
+            (* HACK: do not record the history of values in the pre as they are unused *)
+            let foot_stack = BaseStack.add var (addr, []) (astate.pre :> base_domain).stack in
+            let foot_heap = BaseMemory.register_address addr (astate.pre :> base_domain).heap in
             InvertedDomain.make foot_stack foot_heap
           else astate.pre
         in
@@ -152,53 +155,56 @@ module Memory = struct
 
 
   (** if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
-  let record_must_be_valid action address (pre : InvertedDomain.t) =
+  let record_must_be_valid access_trace address (pre : InvertedDomain.t) =
     if BaseMemory.mem_edges address (pre :> base_domain).heap then
       InvertedDomain.update pre
-        ~heap:(BaseMemory.add_attribute address (MustBeValid action) (pre :> base_domain).heap)
+        ~heap:
+          (BaseMemory.add_attribute address (MustBeValid access_trace) (pre :> base_domain).heap)
     else pre
 
 
-  let check_valid action addr ({post; pre} as astate) =
+  let check_valid access_trace addr ({post; pre} as astate) =
     BaseMemory.check_valid addr (post :> base_domain).heap
     >>| fun () ->
-    let new_pre = record_must_be_valid action addr pre in
+    let new_pre = record_must_be_valid access_trace addr pre in
     if phys_equal new_pre pre then astate else {astate with pre= new_pre}
 
 
-  let add_edge addr access new_addr_trace loc astate =
+  let add_edge (addr, history) access new_addr_hist location astate =
     map_post_heap astate ~f:(fun heap ->
-        BaseMemory.add_edge addr access new_addr_trace heap
-        |> BaseMemory.add_attribute addr
-             (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc})) )
+        BaseMemory.add_edge addr access new_addr_hist heap
+        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history}))
+    )
 
 
   let find_edge_opt address access astate =
     BaseMemory.find_edge_opt address access (astate.post :> base_domain).heap
 
 
-  let eval_edge addr access astate =
-    match find_edge_opt addr access astate with
-    | Some addr_trace' ->
-        (astate, addr_trace')
+  let eval_edge (addr_src, hist_src) access astate =
+    match find_edge_opt addr_src access astate with
+    | Some addr_hist_dst ->
+        (astate, addr_hist_dst)
     | None ->
-        let addr_trace' = (AbstractAddress.mk_fresh (), []) in
+        let addr_dst = AbstractAddress.mk_fresh () in
+        let addr_hist_dst = (addr_dst, hist_src) in
         let post_heap =
-          BaseMemory.add_edge addr access addr_trace' (astate.post :> base_domain).heap
+          BaseMemory.add_edge addr_src access addr_hist_dst (astate.post :> base_domain).heap
         in
         let foot_heap =
-          if BaseMemory.mem_edges addr (astate.pre :> base_domain).heap then
-            BaseMemory.add_edge addr access addr_trace' (astate.pre :> base_domain).heap
-            |> BaseMemory.register_address (fst addr_trace')
+          if BaseMemory.mem_edges addr_src (astate.pre :> base_domain).heap then
+            (* HACK: do not record the history of values in the pre as they are unused *)
+            BaseMemory.add_edge addr_src access (addr_dst, []) (astate.pre :> base_domain).heap
+            |> BaseMemory.register_address addr_dst
           else (astate.pre :> base_domain).heap
         in
         ( { post= Domain.update astate.post ~heap:post_heap
           ; pre= InvertedDomain.update astate.pre ~heap:foot_heap }
-        , addr_trace' )
+        , addr_hist_dst )
 
 
-  let invalidate address action astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address action heap)
+  let invalidate address invalidation location astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address invalidation location heap)
 
 
   let add_attribute address attributes astate =
@@ -221,11 +227,11 @@ module Memory = struct
 
   let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap
 
-  let set_cell addr cell loc astate =
+  let set_cell (addr, history) cell location astate =
     map_post_heap astate ~f:(fun heap ->
         BaseMemory.set_cell addr cell heap
-        |> BaseMemory.add_attribute addr
-             (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc})) )
+        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history}))
+    )
 
 
   module Edges = BaseMemory.Edges
@@ -241,8 +247,7 @@ let mk_initial proc_desc =
     |> List.map ~f:(fun (mangled, _) ->
            let pvar = Pvar.mk mangled proc_name in
            ( Var.of_pvar pvar
-           , ( AbstractAddress.mk_fresh ()
-             , [PulseDomain.ValueHistory.FormalDeclared (pvar, location)] ) ) )
+           , (AbstractAddress.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) )
   in
   let initial_stack =
     List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack
@@ -305,11 +310,10 @@ module PrePost = struct
 
 
   let add_out_of_scope_attribute addr pvar location history heap typ =
-    let action =
-      PulseDomain.InterprocAction.Immediate
-        {imm= PulseDomain.Invalidation.GoneOutOfScope (pvar, typ); location}
+    let attr =
+      Attribute.Invalid (Immediate {imm= GoneOutOfScope (pvar, typ); location; history})
     in
-    BaseMemory.add_attribute addr (Invalid {action; history}) heap
+    BaseMemory.add_attribute addr attr heap
 
 
   (** invalidate local variables going out of scope *)
@@ -356,8 +360,8 @@ module PrePost = struct
   (** stuff we carry around when computing the result of applying one pre/post pair *)
   type call_state =
     { astate: t  (** caller's abstract state computed so far *)
-    ; subst: AbstractAddress.t AddressMap.t
-          (** translation from callee addresses to caller addresses *)
+    ; subst: (AbstractAddress.t * ValueHistory.t) AddressMap.t
+          (** translation from callee addresses to caller addresses and their caller histories *)
     ; rev_subst: AbstractAddress.t AddressMap.t
           (** the inverse translation from [subst] from caller addresses to callee addresses *)
     ; visited: AddressSet.t
@@ -373,28 +377,31 @@ module PrePost = struct
       "@[<v>{ astate=@[<hv2>%a@];@, subst=@[<hv2>%a@];@, rev_subst=@[<hv2>%a@];@, \
        visited=@[<hv2>%a@]@, }@]"
       pp astate
-      (AddressMap.pp ~pp_value:AbstractAddress.pp)
+      (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractAddress.pp fmt addr))
       subst
       (AddressMap.pp ~pp_value:AbstractAddress.pp)
       rev_subst AddressSet.pp visited
 
 
-  let fold_globals_of_stack stack call_state ~f =
+  let fold_globals_of_stack call_loc stack call_state ~f =
     Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold)
       stack ~init:call_state ~f:(fun call_state (var, stack_value) ->
         match var with
         | Var.ProgramVar pvar when Pvar.is_global pvar ->
-            let call_state, (addr_caller, _) =
-              let astate, var_value = Stack.eval var call_state.astate in
+            let call_state, addr_hist_caller =
+              let astate, var_value =
+                Stack.eval [ValueHistory.VariableAccessed (pvar, call_loc)] var call_state.astate
+              in
               if phys_equal astate call_state.astate then (call_state, var_value)
               else ({call_state with astate}, var_value)
             in
-            f pvar ~stack_value ~addr_caller call_state
+            f pvar ~stack_value ~addr_hist_caller call_state
         | _ ->
             Ok call_state )
 
 
-  let visit call_state ~addr_callee ~addr_caller =
+  let visit call_state ~addr_callee ~addr_hist_caller =
+    let addr_caller = fst addr_hist_caller in
     ( match AddressMap.find_opt addr_caller call_state.rev_subst with
     | Some addr_callee' when not (AbstractAddress.equal addr_callee addr_callee') ->
         L.d_printfln "Huho, address %a in post already bound to %a, not %a@\nState=%a"
@@ -408,7 +415,7 @@ module PrePost = struct
       ( `NotAlreadyVisited
       , { call_state with
           visited= AddressSet.add addr_callee call_state.visited
-        ; subst= AddressMap.add addr_callee addr_caller call_state.subst
+        ; subst= AddressMap.add addr_callee addr_hist_caller call_state.subst
         ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } )
 
 
@@ -422,13 +429,16 @@ module PrePost = struct
   (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in
      [call_state.astate] starting from address [addr_caller]. Report an error if some invalid
      addresses are traversed in the process. *)
-  let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_caller
-      history call_state =
-    let mk_action action =
-      PulseDomain.InterprocAction.ViaCall
-        {action; f= Call callee_proc_name; location= call_location}
+  let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre
+      ~addr_hist_caller call_state =
+    let add_call trace =
+      Trace.ViaCall
+        { in_call= trace
+        ; f= Call callee_proc_name
+        ; location= call_location
+        ; history= snd addr_hist_caller }
     in
-    match visit call_state ~addr_callee:addr_pre ~addr_caller with
+    match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with
     | `AlreadyVisited, call_state ->
         Ok call_state
     | `NotAlreadyVisited, call_state -> (
@@ -436,24 +446,23 @@ module PrePost = struct
         BaseMemory.find_opt addr_pre pre.PulseDomain.heap
         >>= fun (edges_pre, attrs_pre) ->
         Attributes.get_must_be_valid attrs_pre
-        >>| fun callee_action ->
-        let action = mk_action callee_action in
-        match Memory.check_valid action addr_caller call_state.astate with
+        >>| fun callee_access_trace ->
+        let access_trace = add_call callee_access_trace in
+        match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with
         | Error invalidated_by ->
             Error
-              (PulseDiagnostic.AccessToInvalidAddress
-                 {invalidated_by; accessed_by= {action; history}})
+              (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace})
         | Ok astate ->
             let call_state = {call_state with astate} in
             Container.fold_result
               ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold)
               ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) ->
-                let astate, (addr_caller_dest, _) =
-                  Memory.eval_edge addr_caller access call_state.astate
+                let astate, addr_hist_dest_caller =
+                  Memory.eval_edge addr_hist_caller access call_state.astate
                 in
                 let call_state = {call_state with astate} in
                 materialize_pre_from_address callee_proc_name call_location ~pre
-                  ~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest history call_state ))
+                  ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state ))
         |> function Some result -> result | None -> Ok call_state )
 
 
@@ -461,15 +470,14 @@ module PrePost = struct
       has been instantiated with the corresponding [actual] into the current state
       [call_state.astate] *)
   let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state =
-    let addr_caller, trace = actual in
-    L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp addr_caller ;
+    L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp (fst actual) ;
     (let open Option.Monad_infix in
     BaseStack.find_opt formal pre.PulseDomain.stack
     >>= fun (addr_formal_pre, _) ->
     BaseMemory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap
     >>| fun (formal_pre, _) ->
     materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre
-      ~addr_caller trace call_state)
+      ~addr_hist_caller:actual call_state)
     |> function Some result -> result | None -> Ok call_state
 
 
@@ -514,11 +522,11 @@ module PrePost = struct
 
 
   let materialize_pre_for_globals callee_proc_name call_location pre_post call_state =
-    fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state
-      ~f:(fun _var ~stack_value:(addr_pre, history) ~addr_caller call_state ->
+    fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state
+      ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state ->
         materialize_pre_from_address callee_proc_name call_location
           ~pre:(pre_post.pre :> PulseDomain.t)
-          ~addr_pre ~addr_caller history call_state )
+          ~addr_pre ~addr_hist_caller call_state )
 
 
   let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state =
@@ -537,19 +545,21 @@ module PrePost = struct
 
   (* {3 applying the post to the current state} *)
 
-  let subst_find_or_new subst addr_callee =
+  let subst_find_or_new subst addr_callee ~default_hist_caller =
     match AddressMap.find_opt addr_callee subst with
     | None ->
-        let addr_fresh = AbstractAddress.mk_fresh () in
-        (addr_fresh, AddressMap.add addr_callee addr_fresh subst)
-    | Some addr_caller ->
-        (addr_caller, subst)
+        let addr_hist_fresh = (AbstractAddress.mk_fresh (), default_hist_caller) in
+        (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh)
+    | Some addr_hist_caller ->
+        (subst, addr_hist_caller)
 
 
-  let call_state_subst_find_or_new call_state addr_callee =
-    let addr_caller, new_subst = subst_find_or_new call_state.subst addr_callee in
-    if phys_equal new_subst call_state.subst then (call_state, addr_caller)
-    else ({call_state with subst= new_subst}, addr_caller)
+  let call_state_subst_find_or_new call_state addr_callee ~default_hist_caller =
+    let new_subst, addr_hist_caller =
+      subst_find_or_new call_state.subst addr_callee ~default_hist_caller
+    in
+    if phys_equal new_subst call_state.subst then (call_state, addr_hist_caller)
+    else ({call_state with subst= new_subst}, addr_hist_caller)
 
 
   let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~cell_pre_opt ~addr_caller call_state =
@@ -572,14 +582,15 @@ module PrePost = struct
             old_post_edges edges_pre )
 
 
-  let add_call_to_attr proc_name location attr =
+  let add_call_to_attr proc_name call_location caller_history attr =
     match (attr : Attribute.t) with
-    | Invalid trace ->
+    | Invalid invalidation ->
         Attribute.Invalid
-          { action=
-              PulseDomain.InterprocAction.ViaCall
-                {action= trace.action; f= Call proc_name; location}
-          ; history= trace.history }
+          (ViaCall
+             { f= Call proc_name
+             ; location= call_location
+             ; history= caller_history
+             ; in_call= invalidation })
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
     | Closure _
@@ -591,25 +602,28 @@ module PrePost = struct
 
 
   let record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
-      ~cell_post:(edges_post, attrs_post) ~addr_caller call_state =
+      ~cell_post:(edges_post, attrs_post) ~addr_hist_caller:(addr_caller, hist_caller) call_state =
     let post_edges_minus_pre =
       delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state
     in
     let heap = (call_state.astate.post :> base_domain).heap in
     let heap =
       let attrs_post_caller =
-        Attributes.map ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr) attrs_post
+        Attributes.map attrs_post ~f:(fun attr ->
+            add_call_to_attr callee_proc_name call_loc hist_caller attr )
       in
       BaseMemory.set_attrs addr_caller attrs_post_caller heap
     in
     let subst, translated_post_edges =
       BaseMemory.Edges.fold_map ~init:call_state.subst edges_post
         ~f:(fun subst (addr_callee, trace_post) ->
-          let addr_curr, subst = subst_find_or_new subst addr_callee in
+          let subst, (addr_curr, hist_curr) =
+            subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller
+          in
           ( subst
           , ( addr_curr
-            , PulseDomain.ValueHistory.Call {f= Call callee_proc_name; location= call_loc}
-              :: trace_post ) ) )
+            , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post}
+              :: hist_curr ) ) )
     in
     let heap =
       let edges_post_caller =
@@ -618,14 +632,23 @@ module PrePost = struct
           post_edges_minus_pre translated_post_edges
       in
       let written_to =
-        (let open Option.Monad_infix in
+        let open Option.Monad_infix in
         BaseMemory.find_opt addr_caller heap
-        >>= fun (_edges, attrs) ->
-        Attributes.get_written_to attrs
-        >>| fun callee_action ->
+        >>= (fun (_edges, attrs) -> Attributes.get_written_to attrs)
+        |> fun written_to_callee_opt ->
+        let callee_trace =
+          match written_to_callee_opt with
+          | None ->
+              Trace.Immediate {imm= (); location= call_loc; history= []}
+          | Some access_trace ->
+              access_trace
+        in
         Attribute.WrittenTo
-          (ViaCall {action= callee_action; f= Call callee_proc_name; location= call_loc}))
-        |> Option.value ~default:(Attribute.WrittenTo (Immediate {imm= (); location= call_loc}))
+          (ViaCall
+             { in_call= callee_trace
+             ; f= Call callee_proc_name
+             ; location= call_loc
+             ; history= hist_caller })
       in
       BaseMemory.set_edges addr_caller edges_post_caller heap
       |> BaseMemory.add_attribute addr_caller written_to
@@ -635,9 +658,9 @@ module PrePost = struct
 
 
   let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee
-      ~addr_caller call_state =
-    L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ;
-    match visit call_state ~addr_callee ~addr_caller with
+      ~addr_hist_caller call_state =
+    L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp (fst addr_hist_caller) ;
+    match visit call_state ~addr_callee ~addr_hist_caller with
     | `AlreadyVisited, call_state ->
         call_state
     | `NotAlreadyVisited, call_state -> (
@@ -651,23 +674,23 @@ module PrePost = struct
           let call_state_after_post =
             if is_cell_read_only ~cell_pre_opt ~cell_post then call_state
             else
-              record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt ~addr_caller
-                ~cell_post call_state
+              record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
+                ~addr_hist_caller ~cell_post call_state
           in
           IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold
             ~init:call_state_after_post edges_post
             ~f:(fun call_state (_access, (addr_callee_dest, _)) ->
-              let call_state, addr_curr_dest =
+              let call_state, addr_hist_curr_dest =
                 call_state_subst_find_or_new call_state addr_callee_dest
+                  ~default_hist_caller:(snd addr_hist_caller)
               in
               record_post_for_address callee_proc_name call_loc pre_post
-                ~addr_callee:addr_callee_dest ~addr_caller:addr_curr_dest call_state ) )
+                ~addr_callee:addr_callee_dest ~addr_hist_caller:addr_hist_curr_dest call_state ) )
 
 
   let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state =
-    let addr_caller, _ = actual in
     L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractAddress.pp
-      addr_caller ;
+      (fst actual) ;
     match
       let open Option.Monad_infix in
       BaseStack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack
@@ -676,7 +699,7 @@ module PrePost = struct
         (pre_post.pre :> PulseDomain.t).PulseDomain.heap
       >>| fun (formal_pre, _) ->
       record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
-        ~addr_caller call_state
+        ~addr_hist_caller:actual call_state
     with
     | Some call_state ->
         call_state
@@ -697,18 +720,19 @@ module PrePost = struct
       | None ->
           (call_state, None)
       | Some (return_callee, _) ->
-          let return_caller =
+          let return_caller_addr_hist =
             match AddressMap.find_opt return_callee call_state.subst with
-            | Some return_caller ->
-                return_caller
+            | Some return_caller_hist ->
+                return_caller_hist
             | None ->
-                AbstractAddress.mk_fresh ()
+                ( AbstractAddress.mk_fresh ()
+                , [ (* this could maybe include an event like "returned here" *) ] )
           in
           let call_state =
             record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee
-              ~addr_caller:return_caller call_state
+              ~addr_hist_caller:return_caller_addr_hist call_state
           in
-          (call_state, Some return_caller) )
+          (call_state, Some return_caller_addr_hist) )
 
 
   let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
@@ -732,11 +756,11 @@ module PrePost = struct
 
   let apply_post_for_globals callee_proc_name call_location pre_post call_state =
     match
-      fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state
-        ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_caller call_state ->
+      fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state
+        ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state ->
           Ok
             (record_post_for_address callee_proc_name call_location pre_post ~addr_callee
-               ~addr_caller call_state) )
+               ~addr_hist_caller call_state) )
     with
     | Error _ ->
         (* always return [Ok _] above *) assert false
@@ -755,10 +779,10 @@ module PrePost = struct
             match AddressMap.find_opt addr_callee call_state.subst with
             | None ->
                 (* callee address has no meaning for the caller *) heap
-            | Some addr_caller ->
+            | Some (addr_caller, history) ->
                 let attrs' =
                   Attributes.map
-                    ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr)
+                    ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc history attr)
                     attrs
                 in
                 BaseMemory.set_attrs addr_caller attrs' heap )
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 7cf77765a..fc325e72c 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -7,6 +7,9 @@
 open! IStd
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
+module Invalidation = PulseDomain.Invalidation
+module Trace = PulseDomain.Trace
+module ValueHistory = PulseDomain.ValueHistory
 
 (* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition
    when necessary
@@ -29,7 +32,7 @@ module Stack : sig
 
   val find_opt : Var.t -> t -> PulseDomain.Stack.value option
 
-  val eval : Var.t -> t -> t * PulseDomain.AddrTracePair.t
+  val eval : ValueHistory.t -> Var.t -> t -> t * PulseDomain.AddrTracePair.t
   (** return the value of the variable in the stack or create a fresh one if needed *)
 
   val mem : Var.t -> t -> bool
@@ -46,25 +49,23 @@ module Memory : sig
   val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t
 
   val add_edge :
-    AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> Location.t -> t -> t
-
-  val check_valid :
-       unit PulseDomain.InterprocAction.t
-    -> AbstractAddress.t
+       AbstractAddress.t * ValueHistory.t
+    -> Access.t
+    -> PulseDomain.AddrTracePair.t
+    -> Location.t
+    -> t
     -> t
-    -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result
+
+  val check_valid : unit Trace.t -> AbstractAddress.t -> t -> (t, Invalidation.t Trace.t) result
 
   val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option
 
   val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option
 
-  val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> Location.t -> t -> t
+  val set_cell :
+    AbstractAddress.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t
 
-  val invalidate :
-       AbstractAddress.t * PulseDomain.ValueHistory.t
-    -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-    -> t
-    -> t
+  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
   val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
 
@@ -72,9 +73,10 @@ module Memory : sig
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 
-  val eval_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
-  (** [eval_edge addr access astate] follows the edge [addr --access--> .] in memory and returns
-      what it points to or creates a fresh value if that edge didn't exist.  *)
+  val eval_edge :
+    AbstractAddress.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
+  (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and
+      returns what it points to or creates a fresh value if that edge didn't exist.  *)
 
   val get_constant : AbstractAddress.t -> t -> Const.t option
 end
@@ -95,9 +97,9 @@ module PrePost : sig
     -> Location.t
     -> t
     -> formals:Var.t list
-    -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list
+    -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list
     -> domain_t
-    -> (domain_t * AbstractAddress.t option, PulseDiagnostic.t) result
+    -> (domain_t * (AbstractAddress.t * ValueHistory.t) option, PulseDiagnostic.t) result
   (** return the abstract state after the call along with an optional return value *)
 end
 
diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml
index cc33cc9be..cf5fa393a 100644
--- a/infer/src/pulse/PulseDiagnostic.ml
+++ b/infer/src/pulse/PulseDiagnostic.ml
@@ -7,25 +7,24 @@
 
 open! IStd
 module F = Format
+module CallEvent = PulseDomain.CallEvent
+module Invalidation = PulseDomain.Invalidation
+module Trace = PulseDomain.Trace
+module ValueHistory = PulseDomain.ValueHistory
 
 type t =
-  | AccessToInvalidAddress of
-      { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
-      ; accessed_by: unit PulseDomain.Trace.t }
-  | StackVariableAddressEscape of
-      { variable: Var.t
-      ; history: PulseDomain.ValueHistory.t
-      ; location: Location.t }
+  | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}
+  | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 let get_location = function
   | AccessToInvalidAddress {accessed_by} ->
-      PulseDomain.InterprocAction.to_outer_location accessed_by.action
+      Trace.get_outer_location accessed_by
   | StackVariableAddressEscape {location} ->
       location
 
 
 let get_message = function
-  | AccessToInvalidAddress {accessed_by; invalidated_by; _} ->
+  | AccessToInvalidAddress {accessed_by; invalidated_by} ->
       (* The goal is to get one of the following messages depending on the scenario:
 
          42: delete x; return x->f
@@ -43,31 +42,27 @@ let get_message = function
          Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then
          "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
       *)
-      let pp_access_trace fmt (trace : _ PulseDomain.Trace.t) =
-        match trace.action with
-        | Immediate {imm= _; _} ->
+      let pp_access_trace fmt (trace : unit Trace.t) =
+        match trace with
+        | Immediate {imm= (); _} ->
             F.fprintf fmt "accessing memory that "
         | ViaCall {f; _} ->
-            F.fprintf fmt "call to %a eventually accesses memory that "
-              PulseDomain.CallEvent.describe f
+            F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f
       in
-      let pp_invalidation_trace line fmt trace =
-        match trace.PulseDomain.Trace.action with
-        | Immediate {imm= invalidation; _} ->
-            F.fprintf fmt "%a on line %d" PulseDomain.Invalidation.describe invalidation line
-        | ViaCall {action; f; _} ->
-            F.fprintf fmt "%a on line %d indirectly during the call to %a"
-              PulseDomain.Invalidation.describe
-              (PulseDomain.InterprocAction.get_immediate action)
-              line PulseDomain.CallEvent.describe f
+      let pp_invalidation_trace line fmt (trace : Invalidation.t Trace.t) =
+        let pp_line fmt line = F.fprintf fmt " on line %d" line in
+        match trace with
+        | ViaCall {f; in_call} ->
+            let invalid = Trace.get_immediate in_call in
+            F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalid
+              pp_line line CallEvent.describe f
+        | Immediate {imm= invalid} ->
+            F.fprintf fmt "%a%a" Invalidation.describe invalid pp_line line
       in
-      let line_of_trace trace =
-        let {Location.line; _} =
-          PulseDomain.InterprocAction.to_outer_location trace.PulseDomain.Trace.action
-        in
+      let invalidation_line =
+        let {Location.line; _} = Trace.get_outer_location invalidated_by in
         line
       in
-      let invalidation_line = line_of_trace invalidated_by in
       F.asprintf "%a%a" pp_access_trace accessed_by
         (pp_invalidation_trace invalidation_line)
         invalidated_by
@@ -79,18 +74,29 @@ let get_message = function
       F.asprintf "address of %a is returned by the function" pp_var variable
 
 
+let add_errlog_header ~title location errlog =
+  let depth = 0 in
+  let tags = [] in
+  Errlog.make_trace_element depth location title tags :: errlog
+
+
 let get_trace = function
   | AccessToInvalidAddress {accessed_by; invalidated_by} ->
-      PulseDomain.Trace.add_to_errlog ~header:"invalidation part of the trace starts here"
-        (fun f invalidation ->
-          F.fprintf f "memory %a here" PulseDomain.Invalidation.describe invalidation )
-        invalidated_by
-      @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here"
-           (fun f () -> F.pp_print_string f "invalid access occurs here")
+      let start_location = Trace.get_start_location invalidated_by in
+      add_errlog_header ~title:"invalidation part of the trace starts here" start_location
+      @@ Trace.add_to_errlog ~nesting:1
+           (fun fmt invalid -> F.fprintf fmt "%a" Invalidation.describe invalid)
+           invalidated_by
+      @@
+      let access_start_location = Trace.get_start_location accessed_by in
+      add_errlog_header ~title:"use-after-lifetime part of the trace starts here"
+        access_start_location
+      @@ Trace.add_to_errlog ~nesting:1
+           (fun fmt () -> F.pp_print_string fmt "invalid access occurs here")
            accessed_by
       @@ []
   | StackVariableAddressEscape {history; location; _} ->
-      PulseDomain.ValueHistory.add_to_errlog ~nesting:0 history
+      ValueHistory.add_to_errlog ~nesting:0 history
       @@
       let nesting = 0 in
       [Errlog.make_trace_element nesting location "returned here" []]
@@ -98,7 +104,6 @@ let get_trace = function
 
 let get_issue_type = function
   | AccessToInvalidAddress {invalidated_by} ->
-      PulseDomain.InterprocAction.get_immediate invalidated_by.action
-      |> PulseDomain.Invalidation.issue_type_of_cause
+      Trace.get_immediate invalidated_by |> Invalidation.issue_type_of_cause
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape
diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli
index 090726cac..9f7652b46 100644
--- a/infer/src/pulse/PulseDiagnostic.mli
+++ b/infer/src/pulse/PulseDiagnostic.mli
@@ -6,16 +6,14 @@
  *)
 
 open! IStd
+module Invalidation = PulseDomain.Invalidation
+module Trace = PulseDomain.Trace
+module ValueHistory = PulseDomain.ValueHistory
 
 (** an error to report to the user *)
 type t =
-  | AccessToInvalidAddress of
-      { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
-      ; accessed_by: unit PulseDomain.Trace.t }
-  | StackVariableAddressEscape of
-      { variable: Var.t
-      ; history: PulseDomain.ValueHistory.t
-      ; location: Location.t }
+  | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}
+  | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 val get_message : t -> string
 
diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml
index a057a2823..bc2b9e94d 100644
--- a/infer/src/pulse/PulseDomain.ml
+++ b/infer/src/pulse/PulseDomain.ml
@@ -124,18 +124,26 @@ end
 module ValueHistory = struct
   type event =
     | Assignment of Location.t
-    | Call of {f: CallEvent.t; location: Location.t}
+    | Call of {f: CallEvent.t; location: Location.t; in_call: t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
     | CppTemporaryCreated of Location.t
     | FormalDeclared of Pvar.t * Location.t
+    | VariableAccessed of Pvar.t * Location.t
     | VariableDeclared of Pvar.t * Location.t
-  [@@deriving compare]
 
-  let pp_event_no_location fmt = function
+  and t = event list [@@deriving compare]
+
+  let pp_event_no_location fmt event =
+    let pp_pvar fmt pvar =
+      if Pvar.is_global pvar then
+        F.fprintf fmt "global variable `%a`" Pvar.pp_value_non_verbose pvar
+      else F.fprintf fmt "variable `%a`" Pvar.pp_value_non_verbose pvar
+    in
+    match event with
     | Assignment _ ->
         F.pp_print_string fmt "assigned"
     | Call {f; location= _} ->
-        F.fprintf fmt "returned from call to %a" CallEvent.pp f
+        F.fprintf fmt "passed as argument to %a" CallEvent.pp f
     | Capture {captured_as; location= _} ->
         F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as
     | CppTemporaryCreated _ ->
@@ -146,8 +154,10 @@ module ValueHistory = struct
           |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Typ.Procname.pp proc_name)
         in
         F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar
+    | VariableAccessed (pvar, _) ->
+        F.fprintf fmt "%a accessed here" pp_pvar pvar
     | VariableDeclared (pvar, _) ->
-        F.fprintf fmt "variable `%a` declared here" Pvar.pp_value_non_verbose pvar
+        F.fprintf fmt "%a declared here" pp_pvar pvar
 
 
   let location_of_event = function
@@ -156,105 +166,115 @@ module ValueHistory = struct
     | Capture {location}
     | CppTemporaryCreated location
     | FormalDeclared (_, location)
+    | VariableAccessed (_, location)
     | VariableDeclared (_, location) ->
         location
 
 
-  let pp_event fmt crumb =
-    F.fprintf fmt "%a at %a" pp_event_no_location crumb Location.pp_line (location_of_event crumb)
-
-
-  let errlog_trace_elem_of_event ~nesting crumb =
-    let location = location_of_event crumb in
-    let description = F.asprintf "%a" pp_event_no_location crumb in
-    let tags = [] in
-    Errlog.make_trace_element nesting location description tags
+  let pp_event fmt event =
+    F.fprintf fmt "%a at %a" pp_event_no_location event Location.pp_line (location_of_event event)
 
 
-  type t = event list [@@deriving compare]
+  let pp fmt history =
+    let rec pp_aux fmt = function
+      | [] ->
+          ()
+      | (Call {f; in_call} as event) :: tail ->
+          F.fprintf fmt "%a@;" pp_event event ;
+          F.fprintf fmt "[%a]@;" pp_aux (List.rev in_call) ;
+          if not (List.is_empty tail) then F.fprintf fmt "return from call to %a@;" CallEvent.pp f ;
+          pp_aux fmt tail
+      | event :: tail ->
+          F.fprintf fmt "%a@;" pp_event event ;
+          pp_aux fmt tail
+    in
+    F.fprintf fmt "@[%a@]" pp_aux (List.rev history)
 
-  let pp f events = Pp.seq ~print_env:Pp.text_break pp_event f events
 
-  let add_to_errlog ~nesting events errlog =
-    List.rev_map_append ~f:(errlog_trace_elem_of_event ~nesting) events errlog
+  let add_event_to_errlog ~nesting event errlog =
+    let location = location_of_event event in
+    let description = F.asprintf "%a" pp_event_no_location event in
+    let tags = [] in
+    Errlog.make_trace_element nesting location description tags :: errlog
 
 
-  let get_start_location = function [] -> None | crumb :: _ -> Some (location_of_event crumb)
+  let add_returned_from_call_to_errlog ~nesting f location errlog =
+    let description = F.asprintf "return from call to %a" CallEvent.pp f in
+    let tags = [] in
+    Errlog.make_trace_element nesting location description tags :: errlog
+
+
+  let add_to_errlog ~nesting history errlog =
+    let rec add_to_errlog_aux ~nesting history errlog =
+      match history with
+      | [] ->
+          errlog
+      | (Call {f; location; in_call} as event) :: tail ->
+          add_to_errlog_aux ~nesting tail
+          @@ add_event_to_errlog ~nesting event
+          @@ add_to_errlog_aux ~nesting:(nesting + 1) in_call
+          @@ add_returned_from_call_to_errlog ~nesting f location
+          @@ errlog
+      | event :: tail ->
+          add_to_errlog_aux ~nesting tail @@ add_event_to_errlog ~nesting event @@ errlog
+    in
+    add_to_errlog_aux ~nesting history errlog
 end
 
-module InterprocAction = struct
+module Trace = struct
   type 'a t =
-    | Immediate of {imm: 'a; location: Location.t}
-    | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.t}
+    | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t}
+    | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: 'a t}
   [@@deriving compare]
 
-  let dummy = Immediate {imm= (); location= Location.dummy}
+  (** only for use in the attributes' [*_rank] functions *)
+  let mk_dummy imm = Immediate {imm; location= Location.dummy; history= []}
 
   let rec get_immediate = function
     | Immediate {imm; _} ->
         imm
-    | ViaCall {action; _} ->
-        get_immediate action
+    | ViaCall {in_call; _} ->
+        get_immediate in_call
 
 
-  let pp pp_immediate fmt = function
-    | Immediate {imm; _} ->
-        pp_immediate fmt imm
-    | ViaCall {f; action; _} ->
-        F.fprintf fmt "%a in call to %a" pp_immediate (get_immediate action) CallEvent.pp f
-
-
-  let add_to_errlog ~nesting pp_immediate action errlog =
-    let rec aux ~nesting rev_errlog action =
-      match action with
-      | Immediate {imm; location} ->
-          let rev_errlog =
-            Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
-            :: rev_errlog
-          in
-          List.rev_append rev_errlog errlog
-      | ViaCall {action; f; location} ->
-          aux ~nesting:(nesting + 1)
-            ( Errlog.make_trace_element nesting location
-                (F.asprintf "when calling %a here" CallEvent.pp f)
-                []
-            :: rev_errlog )
-            action
-    in
-    aux ~nesting [] action
+  let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location
 
+  let get_history = function Immediate {history; _} | ViaCall {history; _} -> history
 
-  let to_outer_location = function Immediate {location} | ViaCall {location} -> location
-end
-
-module Trace = struct
-  type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
-
-  let pp pp_immediate f {action; history} =
-    if Config.debug_level_analysis < 3 then InterprocAction.pp pp_immediate f action
-    else
-      F.fprintf f "{@[action=@[%a@]@;history=@[%a@]@]}" (InterprocAction.pp pp_immediate) action
-        ValueHistory.pp history
-
-
-  let add_errlog_header ~title location errlog =
-    let depth = 0 in
-    let tags = [] in
-    Errlog.make_trace_element depth location title tags :: errlog
-
-
-  let add_to_errlog ~header pp_immediate trace errlog =
-    let start_location =
-      match ValueHistory.get_start_location trace.history with
-      | Some location ->
-          location
-      | None ->
-          InterprocAction.to_outer_location trace.action
-    in
-    add_errlog_header ~title:header start_location
-    @@ ValueHistory.add_to_errlog ~nesting:1 trace.history
-    @@ InterprocAction.add_to_errlog ~nesting:1 pp_immediate trace.action
-    @@ errlog
+  let get_start_location trace =
+    match get_history trace |> List.last with
+    | Some event ->
+        ValueHistory.location_of_event event
+    | None ->
+        get_outer_location trace
+
+
+  let rec pp pp_immediate fmt = function
+    | Immediate {imm; location= _; history} ->
+        if Config.debug_level_analysis < 3 then pp_immediate fmt imm
+        else F.fprintf fmt "%a::%a" ValueHistory.pp history pp_immediate imm
+    | ViaCall {f; location= _; history; in_call} ->
+        if Config.debug_level_analysis < 3 then pp pp_immediate fmt in_call
+        else
+          F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp pp_immediate)
+            in_call
+
+
+  let rec add_to_errlog ~nesting pp_immediate trace errlog =
+    match trace with
+    | Immediate {imm; location; history} ->
+        ValueHistory.add_to_errlog ~nesting history
+        @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
+           :: errlog
+    | ViaCall {f; location; in_call; history} ->
+        ValueHistory.add_to_errlog ~nesting history
+        @@ (fun errlog ->
+             Errlog.make_trace_element nesting location
+               (F.asprintf "when calling %a here" CallEvent.pp f)
+               []
+             :: errlog )
+        @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call
+        @@ errlog
 end
 
 module Attribute = struct
@@ -272,9 +292,9 @@ module Attribute = struct
     | Closure of Typ.Procname.t
     | Constant of Const.t
     | Invalid of Invalidation.t Trace.t
-    | MustBeValid of unit InterprocAction.t
+    | MustBeValid of unit Trace.t
     | StdVectorReserve
-    | WrittenTo of unit InterprocAction.t
+    | WrittenTo of unit Trace.t
   [@@deriving compare, variants]
 
   let equal = [%compare.equal: t]
@@ -283,7 +303,7 @@ module Attribute = struct
 
   let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun ""))
 
-  let written_to_rank = Variants.to_rank (WrittenTo InterprocAction.dummy)
+  let written_to_rank = Variants.to_rank (WrittenTo (Trace.mk_dummy ()))
 
   let address_of_stack_variable_rank =
     let pname = Typ.Procname.from_string_c_fun "" in
@@ -292,19 +312,19 @@ module Attribute = struct
     Variants.to_rank (AddressOfStackVariable (var, location, []))
 
 
-  let invalid_rank =
-    Variants.to_rank
-      (Invalid
-         {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []})
-
+  let invalid_rank = Variants.to_rank (Invalid (Trace.mk_dummy Invalidation.Nullptr))
 
-  let must_be_valid_rank = Variants.to_rank (MustBeValid InterprocAction.dummy)
+  let must_be_valid_rank = Variants.to_rank (MustBeValid (Trace.mk_dummy ()))
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
   let const_rank = Variants.to_rank (Constant (Const.Cint IntLit.zero))
 
-  let pp f = function
+  let pp f attribute =
+    let pp_string_if_debug string fmt () =
+      if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string
+    in
+    match attribute with
     | AddressOfCppTemporary (var, history) ->
         F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history
     | AddressOfStackVariable (var, location, history) ->
@@ -314,19 +334,13 @@ module Attribute = struct
     | Constant c ->
         F.fprintf f "=%a" (Const.pp Pp.text) c
     | Invalid invalidation ->
-        (Trace.pp Invalidation.pp) f invalidation
+        F.fprintf f "Invalid %a" (Trace.pp Invalidation.pp) invalidation
     | MustBeValid action ->
-        F.fprintf f "MustBeValid (read by %a @ %a)"
-          (InterprocAction.pp (fun _ () -> ()))
-          action Location.pp
-          (InterprocAction.to_outer_location action)
+        F.fprintf f "MustBeValid %a" (Trace.pp (pp_string_if_debug "access")) action
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
     | WrittenTo action ->
-        F.fprintf f "WrittenTo (written by %a @ %a)"
-          (InterprocAction.pp (fun _ () -> ()))
-          action Location.pp
-          (InterprocAction.to_outer_location action)
+        F.fprintf f "WrittenTo %a" (Trace.pp (pp_string_if_debug "mutation")) action
 end
 
 module Attributes = struct
@@ -489,7 +503,7 @@ module Memory : sig
 
   val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t
 
-  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> t -> t
+  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
   val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
 
@@ -553,8 +567,9 @@ end = struct
         (fst memory, Graph.add addr new_attrs (snd memory))
 
 
-  let invalidate (address, history) invalidation memory =
-    add_attribute address (Attribute.Invalid {action= invalidation; history}) memory
+  let invalidate (address, history) invalid location memory =
+    let invalidation = Trace.Immediate {imm= invalid; location; history} in
+    add_attribute address (Attribute.Invalid invalidation) memory
 
 
   let check_valid address memory =
diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli
index 9a4d1d80f..d03b40f56 100644
--- a/infer/src/pulse/PulseDomain.mli
+++ b/infer/src/pulse/PulseDomain.mli
@@ -48,34 +48,39 @@ end
 module ValueHistory : sig
   type event =
     | Assignment of Location.t
-    | Call of {f: CallEvent.t; location: Location.t}
+    | Call of {f: CallEvent.t; location: Location.t; in_call: t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
     | CppTemporaryCreated of Location.t
     | FormalDeclared of Pvar.t * Location.t
+    | VariableAccessed of Pvar.t * Location.t
     | VariableDeclared of Pvar.t * Location.t
 
-  type t = event list [@@deriving compare]
+  and t = event list [@@deriving compare]
 
-  val add_to_errlog :
-    nesting:int -> event list -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list
+  val add_to_errlog : nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list
 end
 
-module InterprocAction : sig
+module Trace : sig
   type 'a t =
-    | Immediate of {imm: 'a; location: Location.t}
-    | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.t}
+    | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t}
+    | ViaCall of
+        { f: CallEvent.t
+        ; location: Location.t  (** location of the call event *)
+        ; history: ValueHistory.t  (** the call involves a value with this prior history *)
+        ; in_call: 'a t  (** last step of the trace is in a call to [f] made at [location] *) }
   [@@deriving compare]
 
-  val get_immediate : 'a t -> 'a
+  val get_outer_location : 'a t -> Location.t
+  (** skip histories and go straight to the where the action is: either the action itself or the
+      call that leads to the action *)
 
-  val to_outer_location : 'a t -> Location.t
-end
+  val get_start_location : 'a t -> Location.t
+  (** initial step in the history if not empty, or else same as {!get_outer_location} *)
 
-module Trace : sig
-  type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
+  val get_immediate : 'a t -> 'a
 
   val add_to_errlog :
-       header:string
+       nesting:int
     -> (F.formatter -> 'a -> unit)
     -> 'a t
     -> Errlog.loc_trace_elem list
@@ -89,20 +94,20 @@ module Attribute : sig
     | Closure of Typ.Procname.t
     | Constant of Const.t
     | Invalid of Invalidation.t Trace.t
-    | MustBeValid of unit InterprocAction.t
+    | MustBeValid of unit Trace.t
     | StdVectorReserve
-    | WrittenTo of unit InterprocAction.t
+    | WrittenTo of unit Trace.t
   [@@deriving compare]
 end
 
 module Attributes : sig
   include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t
 
-  val get_must_be_valid : t -> unit InterprocAction.t option
+  val get_must_be_valid : t -> unit Trace.t option
 
   val get_invalid : t -> Invalidation.t Trace.t option
 
-  val get_written_to : t -> unit InterprocAction.t option
+  val get_written_to : t -> unit Trace.t option
 
   val get_address_of_stack_variable : t -> (Var.t * Location.t * ValueHistory.t) option
 
@@ -183,7 +188,7 @@ module Memory : sig
 
   val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t
 
-  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> t -> t
+  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
   val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
 
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 1f8f7f59f..1d3ffe11b 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -20,16 +20,15 @@ type model = exec_fun
 module Misc = struct
   let shallow_copy model_desc : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= Model model_desc; location} in
+    let event = PulseDomain.ValueHistory.Call {f= Model model_desc; location; in_call= []} in
     ( match actuals with
     | [(dest_pointer_hist, _); (src_pointer_hist, _)] ->
         PulseOperations.eval_access location src_pointer_hist Dereference astate
         >>= fun (astate, obj) ->
         PulseOperations.shallow_copy location obj astate
         >>= fun (astate, obj_copy) ->
-        let obj_hist = snd obj in
         PulseOperations.write_deref location ~ref:dest_pointer_hist
-          ~obj:(obj_copy, event :: obj_hist)
+          ~obj:(fst obj_copy, event :: snd obj_copy)
           astate
     | _ ->
         Ok astate )
@@ -46,9 +45,7 @@ module C = struct
    fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(deleted_access, _)] ->
-        PulseOperations.invalidate location
-          (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CFree; location})
-          deleted_access astate
+        PulseOperations.invalidate location PulseDomain.Invalidation.CFree deleted_access astate
         >>| List.return
     | _ ->
         Ok [astate]
@@ -59,9 +56,8 @@ module Cplusplus = struct
    fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(deleted_access, _)] ->
-        PulseOperations.invalidate location
-          (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CppDelete; location})
-          deleted_access astate
+        PulseOperations.invalidate location PulseDomain.Invalidation.CppDelete deleted_access
+          astate
         >>| List.return
     | _ ->
         Ok [astate]
@@ -69,10 +65,12 @@ module Cplusplus = struct
 
   let placement_new : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= Model "<placement new>()"; location} in
+    let event =
+      PulseDomain.ValueHistory.Call {f= Model "<placement new>()"; location; in_call= []}
+    in
     match List.rev actuals with
-    | ((address, _), _) :: _ ->
-        Ok [PulseOperations.write_id ret_id (address, [event]) astate]
+    | ((address, hist), _) :: _ ->
+        Ok [PulseOperations.write_id ret_id (address, event :: hist) astate]
     | _ ->
         Ok [PulseOperations.havoc_id ret_id [event] astate]
 end
@@ -92,7 +90,9 @@ module StdBasicString = struct
 
   let data : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= Model "std::basic_string::data()"; location} in
+    let event =
+      PulseDomain.ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []}
+    in
     match actuals with
     | [(this_hist, _)] ->
         to_internal_string location this_hist astate
@@ -107,24 +107,15 @@ module StdBasicString = struct
   let destructor : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
     let model = PulseDomain.CallEvent.Model "std::basic_string::~basic_string()" in
-    let call_event = PulseDomain.ValueHistory.Call {f= model; location} in
+    let call_event = PulseDomain.ValueHistory.Call {f= model; location; in_call= []} in
     match actuals with
     | [(this_hist, _)] ->
         to_internal_string location this_hist astate
-        >>= fun (astate, string_addr_hist) ->
-        let invalidation =
-          PulseDomain.InterprocAction.ViaCall
-            { location
-            ; f= model
-            ; action=
-                ViaCall
-                  { location
-                  ; f= Model "deleting the underlying string"
-                  ; action= Immediate {imm= PulseDomain.Invalidation.CppDelete; location} } }
-        in
-        PulseOperations.invalidate_deref location invalidation string_addr_hist astate
+        >>= fun (astate, (string_addr, string_hist)) ->
+        let string_addr_hist = (string_addr, call_event :: string_hist) in
+        PulseOperations.invalidate_deref location CppDelete string_addr_hist astate
         >>= fun astate ->
-        PulseOperations.invalidate location invalidation string_addr_hist astate
+        PulseOperations.invalidate location CppDelete string_addr_hist astate
         >>| fun astate -> [astate]
     | _ ->
         Ok [PulseOperations.havoc_id ret_id [call_event] astate]
@@ -134,7 +125,9 @@ module StdFunction = struct
   let operator_call : model =
    fun ~caller_summary location ~ret ~actuals astate ->
     let havoc_ret (ret_id, _) astate =
-      let event = PulseDomain.ValueHistory.Call {f= Model "std::function::operator()"; location} in
+      let event =
+        PulseDomain.ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []}
+      in
       [PulseOperations.havoc_id ret_id [event] astate]
     in
     match actuals with
@@ -143,9 +136,7 @@ module StdFunction = struct
     | (lambda_ptr_hist, _) :: actuals -> (
         PulseOperations.eval_access location lambda_ptr_hist Dereference astate
         >>= fun (astate, (lambda, _)) ->
-        PulseOperations.Closures.check_captured_addresses
-          (PulseDomain.InterprocAction.Immediate {imm= (); location})
-          lambda astate
+        PulseOperations.Closures.check_captured_addresses location lambda astate
         >>= fun astate ->
         match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with
         | None ->
@@ -178,12 +169,8 @@ module StdVector = struct
   let reallocate_internal_array trace vector vector_f location astate =
     to_internal_array location vector astate
     >>= fun (astate, array_address) ->
-    let invalidation =
-      PulseDomain.InterprocAction.Immediate
-        {imm= PulseDomain.Invalidation.StdVector vector_f; location}
-    in
-    PulseOperations.invalidate_array_elements location invalidation array_address astate
-    >>= PulseOperations.invalidate_deref location invalidation array_address
+    PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate
+    >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address
     >>= PulseOperations.havoc_field location vector internal_array trace
 
 
@@ -196,7 +183,8 @@ module StdVector = struct
             { f=
                 Model
                   (Format.asprintf "%a()" PulseDomain.Invalidation.pp_std_vector_function vector_f)
-            ; location }
+            ; location
+            ; in_call= [] }
         in
         reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
     | _ ->
@@ -205,11 +193,14 @@ module StdVector = struct
 
   let at : model =
    fun ~caller_summary:_ location ~ret ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= Model "std::vector::at()"; location} in
+    let event =
+      PulseDomain.ValueHistory.Call {f= Model "std::vector::at()"; location; in_call= []}
+    in
     match actuals with
     | [(vector, _); (index, _)] ->
         element_of_internal_array location vector (fst index) astate
-        >>| fun (astate, (addr, _)) -> [PulseOperations.write_id (fst ret) (addr, [event]) astate]
+        >>| fun (astate, (addr, hist)) ->
+        [PulseOperations.write_id (fst ret) (addr, event :: hist) astate]
     | _ ->
         Ok [PulseOperations.havoc_id (fst ret) [event] astate]
 
@@ -218,7 +209,9 @@ module StdVector = struct
    fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(vector, _); _value] ->
-        let crumb = PulseDomain.ValueHistory.Call {f= Model "std::vector::reserve()"; location} in
+        let crumb =
+          PulseDomain.ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []}
+        in
         reallocate_internal_array [crumb] vector Reserve location astate
         >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector)
         >>| List.return
@@ -231,7 +224,7 @@ module StdVector = struct
     match actuals with
     | [(vector, _); _value] ->
         let crumb =
-          PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location}
+          PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []}
         in
         if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
           (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index c1b24e332..915abb454 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -9,7 +9,7 @@ module L = Logging
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
 module Attributes = PulseDomain.Attributes
-module InterprocAction = PulseDomain.InterprocAction
+module Trace = PulseDomain.Trace
 module ValueHistory = PulseDomain.ValueHistory
 module Memory = PulseAbductiveDomain.Memory
 module Stack = PulseAbductiveDomain.Stack
@@ -28,10 +28,11 @@ type t = PulseAbductiveDomain.t
 type 'a access_result = ('a, PulseDiagnostic.t) result
 
 (** Check that the [address] is not known to be invalid *)
-let check_addr_access action (address, history) astate =
-  Memory.check_valid action address astate
+let check_addr_access location (address, history) astate =
+  let accessed_by = Trace.Immediate {imm= (); location; history} in
+  Memory.check_valid accessed_by address astate
   |> Result.map_error ~f:(fun invalidated_by ->
-         PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= {action; history}} )
+         PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} )
 
 
 module Closures = struct
@@ -93,45 +94,43 @@ module Closures = struct
               let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in
               Some (address_captured, new_trace) )
     in
-    let closure_addr = AbstractAddress.mk_fresh () in
+    let closure_addr_hist = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in
     let fake_capture_edges = mk_capture_edges captured_addresses in
     let astate =
-      Memory.set_cell closure_addr
+      Memory.set_cell closure_addr_hist
         (fake_capture_edges, Attributes.singleton (Closure pname))
         location astate
     in
-    (astate, (closure_addr, (* TODO: trace *) []))
+    (astate, closure_addr_hist)
 end
 
 let eval_var var astate = Stack.eval var astate
 
-let eval_access location addr_trace access astate =
-  let addr = fst addr_trace in
-  let action = InterprocAction.Immediate {imm= (); location} in
-  check_addr_access action addr_trace astate >>| fun astate -> Memory.eval_edge addr access astate
+let eval_access location addr_hist access astate =
+  check_addr_access location addr_hist astate
+  >>| fun astate -> Memory.eval_edge addr_hist access astate
 
 
 let eval location exp0 astate =
-  let action = InterprocAction.Immediate {imm= (); location} in
   let rec eval exp astate =
     match (exp : Exp.t) with
     | Var id ->
-        Ok (eval_var (Var.of_id id) astate)
+        Ok (eval_var (* error in case of missing history? *) [] (Var.of_id id) astate)
     | Lvar pvar ->
-        Ok (eval_var (Var.of_pvar pvar) astate)
+        Ok (eval_var [ValueHistory.VariableAccessed (pvar, location)] (Var.of_pvar pvar) astate)
     | Lfield (exp', field, _) ->
         eval exp' astate
-        >>= fun (astate, addr_trace) ->
-        check_addr_access action addr_trace astate
-        >>| fun astate -> Memory.eval_edge (fst addr_trace) (FieldAccess field) astate
+        >>= fun (astate, addr_hist) ->
+        check_addr_access location addr_hist astate
+        >>| fun astate -> Memory.eval_edge addr_hist (FieldAccess field) astate
     | Lindex (exp', exp_index) ->
         eval exp_index astate
-        >>= fun (astate, addr_trace_index) ->
+        >>= fun (astate, addr_hist_index) ->
         eval exp' astate
-        >>= fun (astate, addr_trace) ->
-        check_addr_access action addr_trace astate
+        >>= fun (astate, addr_hist) ->
+        check_addr_access location addr_hist astate
         >>| fun astate ->
-        Memory.eval_edge (fst addr_trace) (ArrayAccess (Typ.void, fst addr_trace_index)) astate
+        Memory.eval_edge addr_hist (ArrayAccess (Typ.void, fst addr_hist_index)) astate
     | Closure {name; captured_vars} ->
         List.fold_result captured_vars ~init:(astate, [])
           ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) ->
@@ -219,10 +218,9 @@ let assert_is_true location ~condition astate = eval_cond ~negated:false locatio
 
 let eval_deref location exp astate =
   eval location exp astate
-  >>= fun (astate, addr_trace) ->
-  let action = InterprocAction.Immediate {imm= (); location} in
-  check_addr_access action addr_trace astate
-  >>| fun astate -> Memory.eval_edge (fst addr_trace) Dereference astate
+  >>= fun (astate, addr_hist) ->
+  check_addr_access location addr_hist astate
+  >>| fun astate -> Memory.eval_edge addr_hist Dereference astate
 
 
 let realloc_pvar pvar location astate =
@@ -238,12 +236,9 @@ let havoc_id id loc_opt astate =
   else astate
 
 
-let action_of_address location = InterprocAction.Immediate {imm= (); location}
-
 let write_access location addr_trace_ref access addr_trace_obj astate =
-  let action = action_of_address location in
-  check_addr_access action addr_trace_ref astate
-  >>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj location
+  check_addr_access location addr_trace_ref astate
+  >>| Memory.add_edge addr_trace_ref access addr_trace_obj location
 
 
 let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
@@ -263,18 +258,16 @@ let havoc_field location addr_trace field trace_obj astate =
 
 
 let invalidate location cause addr_trace astate =
-  let action = action_of_address location in
-  check_addr_access action addr_trace astate >>| Memory.invalidate addr_trace cause
+  check_addr_access location addr_trace astate >>| Memory.invalidate addr_trace cause location
 
 
-let invalidate_deref location cause (addr_ref, history) astate =
-  let astate, (addr_obj, _) = Memory.eval_edge addr_ref Dereference astate in
-  invalidate location cause (addr_obj, history) astate
+let invalidate_deref location cause ref_addr_hist astate =
+  let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist Dereference astate in
+  invalidate location cause (addr_obj, snd ref_addr_hist) astate
 
 
 let invalidate_array_elements location cause addr_trace astate =
-  let action = action_of_address location in
-  check_addr_access action addr_trace astate
+  check_addr_access location addr_trace astate
   >>| fun astate ->
   match Memory.find_opt (fst addr_trace) astate with
   | None ->
@@ -284,15 +277,14 @@ let invalidate_array_elements location cause addr_trace astate =
         (fun access dest_addr_trace astate ->
           match (access : Memory.Access.t) with
           | ArrayAccess _ ->
-              Memory.invalidate dest_addr_trace cause astate
+              Memory.invalidate dest_addr_trace cause location astate
           | _ ->
               astate )
         edges astate
 
 
 let shallow_copy location addr_hist astate =
-  let action = action_of_address location in
-  check_addr_access action addr_hist astate
+  check_addr_access location addr_hist astate
   >>| fun astate ->
   let cell =
     match Memory.find_opt (fst addr_hist) astate with
@@ -301,7 +293,7 @@ let shallow_copy location addr_hist astate =
     | Some cell ->
         cell
   in
-  let copy = AbstractAddress.mk_fresh () in
+  let copy = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in
   (Memory.set_cell copy cell location astate, copy)
 
 
@@ -391,11 +383,11 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
           PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
             astate
           >>| fun (post, return_val_opt) ->
-          let event = ValueHistory.Call {f= Call callee_pname; location= call_loc} in
+          let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
           let post =
             match return_val_opt with
-            | Some return_val ->
-                write_id (fst ret) (return_val, [event]) post
+            | Some (return_val, return_hist) ->
+                write_id (fst ret) (return_val, event :: return_hist) post
             | None ->
                 havoc_id (fst ret) [event] post
           in
@@ -403,5 +395,7 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
-      let event = ValueHistory.Call {f= SkippedKnownCall callee_pname; location= call_loc} in
+      let event =
+        ValueHistory.Call {f= SkippedKnownCall callee_pname; location= call_loc; in_call= []}
+      in
       Ok [havoc_id (fst ret) [event] astate]
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index 9719a77ff..344ca622b 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/infer/src/pulse/PulseOperations.mli
@@ -14,7 +14,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result
 
 module Closures : sig
   val check_captured_addresses :
-    unit PulseDomain.InterprocAction.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result
+    Location.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result
   (** assert the validity of the addresses captured by the lambda *)
 end
 
@@ -70,31 +70,22 @@ val write_deref :
 (** write the edge [ref --*--> obj] *)
 
 val invalidate :
-     Location.t
-  -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-  -> PulseDomain.AddrTracePair.t
-  -> t
-  -> t access_result
+  Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result
 (** record that the address is invalid *)
 
 val invalidate_deref :
-     Location.t
-  -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-  -> PulseDomain.AddrTracePair.t
-  -> t
-  -> t access_result
+  Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result
 (** record that what the address points to is invalid *)
 
 val invalidate_array_elements :
-     Location.t
-  -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-  -> PulseDomain.AddrTracePair.t
-  -> t
-  -> t access_result
+  Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result
 (** record that all the array elements that address points to is invalid *)
 
 val shallow_copy :
-  Location.t -> PulseDomain.AddrTracePair.t -> t -> (t * AbstractAddress.t) access_result
+     Location.t
+  -> PulseDomain.AddrTracePair.t
+  -> t
+  -> (t * (AbstractAddress.t * PulseDomain.ValueHistory.t)) access_result
 (** returns the address of a new cell with the same edges as the original *)
 
 val remove_vars : Var.t list -> Location.t -> t -> t
diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp
index ad4243d46..9a5df05bc 100644
--- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp
@@ -1,27 +1,27 @@
-../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<A*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<A*>::operator++,parameter 'this' is modified at line 1390, column 9]
-../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<int*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<int*>::operator++,parameter 'this' is modified at line 1390, column 9]
-codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter 'array' is modified at line 33, column 3]
-codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter 'a' is modified at line 15, column 3,parameter 'a' is modified at line 16, column 3]
-codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter 'b' is modified at line 10, column 3,parameter 'a' is modified at line 9, column 3]
-codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,parameter 'a' is modified when calling `array_mod_impure()` at line 22, column 3,parameter 'a' is modified at line 9, column 3]
-codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter 'array' is modified at line 40, column 60]
-codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter 'array' is modified at line 44, column 3]
-codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,global variable 'a' is modified when calling `modify_global_array_impure()` at line 16, column 3,global variable 'a' is modified at line 12, column 37,global variable 'x' is modified when calling `modify_global_primitive_impure()` at line 15, column 3,global variable 'x' is modified at line 10, column 41]
-codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable 'local_static_var_impure.arr' is modified at line 26, column 3,global variable 'local_static_var_impure.arr' is modified at line 27, column 3]
-codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable 'a' is modified at line 12, column 37]
-codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global variable 'x' is modified at line 33, column 22]
-codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable 'x' is modified at line 10, column 41]
-codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter 's',was invalidated by `delete` here]
+../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<A*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<A*>::operator++,parameter `this` of std::__wrap_iter<A*>::operator++,parameter `this` modified here]
+../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<int*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<int*>::operator++,parameter `this` of std::__wrap_iter<int*>::operator++,parameter `this` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter `array` of alias_mod_impure,assigned,parameter `array` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` of array_mod_both_impure,parameter `a` modified here,parameter `a` of array_mod_both_impure,parameter `a` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` of array_mod_impure,parameter `b` modified here,parameter `a` of array_mod_impure,parameter `a` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,parameter `a` of call_array_mod_impure,when calling `array_mod_impure` here,parameter `a` of array_mod_impure,parameter `a` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter `array` of modify_direct_impure,parameter `array` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter `array` of modify_ptr_impure,assigned,parameter `array` modified here]
+codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,global variable `a` accessed here,when calling `modify_global_array_impure` here,global variable `a` accessed here,global variable `a` modified here,global variable `x` accessed here,when calling `modify_global_primitive_impure` here,global variable `x` accessed here,global variable `x` modified here]
+codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable `local_static_var_impure.arr` accessed here,global variable `local_static_var_impure.arr` modified here,global variable `local_static_var_impure.arr` accessed here,global variable `local_static_var_impure.arr` modified here]
+codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable `a` accessed here,global variable `a` modified here]
+codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global variable `x` accessed here,global variable `x` modified here]
+codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable `x` accessed here,global variable `x` modified here]
+codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter `s` of delete_param_impure,parameter `s` was invalidated by `delete` here]
 codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure]
-codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_impure` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_impure` here,invalid access occurs here]
-codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable 'global_pointer',was invalidated by call to `free()` here]
-codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter 'x',was invalidated by call to `free()` here]
-codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter 's' is modified at line 34, column 3]
-codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter 'x' is modified at line 23, column 44]
-codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter 'pp' is modified at line 27, column 3]
-codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter 'x' is modified at line 8, column 38]
-codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter 'vec' is modified at line 29, column 45]
-codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter 'vec' is modified at line 26, column 44]
-codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter 'vec' is modified at line 8, column 45]
-codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter 'vec' is modified at line 10, column 48]
-codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter 'vec' is modified at line 21, column 5]
+codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,invalid access occurs here]
+codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable `global_pointer` accessed here,global variable `global_pointer` was invalidated by call to `free()` here]
+codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter `x` of free_param_impure,parameter `x` was invalidated by call to `free()` here]
+codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter `s` of reassign_impure,parameter `s` modified here]
+codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter `x` of create_cycle_impure,parameter `x` modified here]
+codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter `pp` of invalidate_local_impure,parameter `pp` modified here]
+codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter `x` of modify_mut_ref_impure,parameter `x` modified here]
+codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec` of assign_impure,parameter `vec` modified here]
+codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec` of clear_impure,parameter `vec` modified here]
+codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` of insert_impure,parameter `vec` modified here]
+codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec` of push_back_impure,parameter `vec` modified here]
+codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec` of push_back_in_loop_impure,parameter `vec` modified here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp
new file mode 100644
index 000000000..93d5ddde6
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp
@@ -0,0 +1,98 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+// Caricature of folly::basic_fbstring without the union between small
+// and medium/large data representations, and with an explicit field
+// for category_ instead of bitmasking part of the data value.
+// ref:
+// https://github.com/facebook/folly/blob/72850c2ebfb94d87bea74d89fcf79f3aaa91a627/folly/FBString.h
+
+enum category {
+  small = 0, // ignore small strings for now
+  medium = 1,
+  large = 2,
+};
+
+void* checkedMalloc(size_t size) {
+  void* ptr = malloc(size);
+  if (ptr == nullptr) {
+    exit(1);
+  }
+  return ptr;
+}
+
+struct LikeFBString {
+  int category_;
+  char* buffer_;
+  size_t size_;
+  unsigned int refcount;
+
+  LikeFBString() {}
+
+  LikeFBString(const LikeFBString& src) {
+    category_ = src.category();
+    switch (src.category_) {
+      case medium:
+        copyMedium(src);
+        break;
+      case large:
+        copyLarge(src);
+        break;
+      default:
+        exit(2);
+    }
+  }
+
+  ~LikeFBString() {
+    if (category() == medium) {
+      free(buffer_);
+    } else {
+      decr_ref_count();
+    }
+  }
+
+  void copySmall(const LikeFBString& src) {}
+
+  void copyMedium(const LikeFBString& src) {
+    buffer_ = (char*)checkedMalloc(src.size_);
+    size_ = src.size_;
+  }
+
+  void copyLarge(const LikeFBString& src) {
+    refcount++;
+    buffer_ = src.buffer_;
+    size_ = src.size_;
+  }
+
+  int category() const { return category_; }
+
+  void incr_ref_count() { refcount++; }
+
+  void decr_ref_count() {
+    refcount--;
+    if (refcount == 0) {
+      free(buffer_);
+    }
+  }
+};
+
+void copy_fbstring(LikeFBString& s) {
+  // this might alias the underlying buffers if the string is large in
+  // that case the destruction of t does not de-allocate its buffer
+  // but pulse might think it does if it fails to remember which
+  // category t belongs to and follows impossibly control flow
+  LikeFBString t = s;
+}
+
+void FP_pass_to_copy_ok() {
+  // Currently pulse follows impossible control flow and thinks the
+  // underlying buffer of s is freed twice: once per copy. That is
+  // caused by manual ref-counting in the case of large strings.
+  LikeFBString s;
+  copy_fbstring(s);
+}
diff --git a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp
index 4fbff9995..0c5710580 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp
@@ -100,8 +100,14 @@ void invalidate_and_set_to_null(struct X** x_ptr) {
   *x_ptr = nullptr;
 }
 
-void access_to_invalidated_alias(struct X* x, struct X* y) {
+void access_to_invalidated_alias_bad(struct X* x, struct X* y) {
   y = x;
   invalidate_and_set_to_null(&x);
   wraps_read(*y);
 }
+
+void access_to_invalidated_alias2_bad(struct X* x, struct X* y) {
+  y = x;
+  invalidate_and_set_to_null(&y);
+  wraps_read(*x);
+}
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index f529bf564..e5f751807 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,64 +1,67 @@
-codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `Range::operator[]` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
-codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_ne_then_eq_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function<_Bool>` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function<int>` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<int>` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `some::thing::bad_ptr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `some::thing::bad_ptr`,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `invalidate_and_set_to_null` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete` here,when calling `wraps_delete_inner` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `may_return_invalid_ptr_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,when calling `store` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,when calling `WrapsB::~WrapsB` here,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `WrapsB::getb`,assigned,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,returned from call to `getwrapperHeap`,invalid access occurs here]
-codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `b` declared here,when calling `getwrapperStack` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack`,returned from call to `getwrapperStack`,invalid access occurs here]
+codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
+codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_ne_then_eq_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here]
+codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function<int>` here,parameter `a` of deduplication::templated_delete_function<int>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<int>` here,parameter `a` of deduplication::templated_access_function<int>,invalid access occurs here]
+codetoanalyze/cpp/pulse/fbstring.cpp, FP_pass_to_copy_ok, 6, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `copy_fbstring` here,parameter `s` of copy_fbstring,passed as argument to `LikeFBString::LikeFBString`,parameter `src` of LikeFBString::LikeFBString,passed as argument to `LikeFBString::copyLarge`,parameter `src` of LikeFBString::copyLarge,assigned,return from call to `LikeFBString::copyLarge`,return from call to `LikeFBString::LikeFBString`,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,when calling `LikeFBString::decr_ref_count` here,parameter `this` of LikeFBString::decr_ref_count,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,invalid access occurs here]
+codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `some::thing::bad_ptr` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `some::thing::bad_ptr`,return from call to `some::thing::bad_ptr`,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_inner_then_write_bad,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_inner_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperHeap` here,variable `a` declared here,passed as argument to `WrapsB::WrapsB`,assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperHeap`,variable `a` declared here,passed as argument to `WrapsB::WrapsB`,assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,assigned,returned here]
-codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `temporaries::UniquePtr<temporaries::A>::~UniquePtr` here,when calling `temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `temporaries::UniquePtr<temporaries::A>::get`,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `<placement new>()` (modelled),assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `<placement new>()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `use_after_destructor::S::operator=`,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `use_after_destructor::S::S`,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `c` declared here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok` here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `t` declared here,when calling `invalidate_local_ok` here,memory is the address of a stack variable `t` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `t` declared here,assigned,returned from call to `invalidate_local_ok`,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr<temporaries::A>::~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::~UniquePtr,when calling `temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr<temporaries::A>::get`,return from call to `temporaries::UniquePtr<temporaries::A>::get`,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,passed as argument to `<placement new>()` (modelled),return from call to `<placement new>()` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,passed as argument to `<placement new>()` (modelled),return from call to `<placement new>()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s2` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s2` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `tmp` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `tmp` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `c` declared here,is the address of a stack variable `c` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
+codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_no_free_if_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_no_free_if_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of insert_bad,was potentially invalidated by `std::vector::insert()`,use-after-lifetime part of the trace starts here,parameter `vec` of insert_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/trace.cpp b/infer/tests/codetoanalyze/cpp/pulse/trace.cpp
new file mode 100644
index 000000000..5db4ec6cb
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/pulse/trace.cpp
@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+void make_alias(int** src, int** dst) { *dst = *src; }
+
+void do_free(int* x) {
+  int* y = x;
+  int* z = y;
+  free(y);
+}
+
+void trace_free_bad(int* x) {
+  int* y;
+  make_alias(&x, &y);
+  do_free(y);
+  int i = *x;
+}
diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp
index 10a59609a..1591496de 100644
--- a/infer/tests/codetoanalyze/java/impurity/issues.exp
+++ b/infer/tests/codetoanalyze/java/impurity/issues.exp
@@ -1,20 +1,20 @@
-codetoanalyze/java/impurity/GlobalTest.java, GlobalTest$Foo.set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest$Foo.set_impure(),global variable 'GlobalTest' is modified at line 16]
-codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.call_set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.call_set_impure(),global variable 'GlobalTest' is modified when calling `GlobalTest$Foo.set_impure()` at line 27,global variable 'GlobalTest' is modified at line 16]
-codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo),global variable 'GlobalTest' is modified when calling `GlobalTest.incr(...)` at line 33,global variable 'GlobalTest' is modified at line 21]
-codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo),global variable 'GlobalTest' is modified when calling `GlobalTest.incr(...)` at line 42,global variable 'GlobalTest' is modified at line 21]
-codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter 'foo' is modified at line 21]
-codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter 'this' is modified at line 67]
-codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter 'this' is modified at line 57]
-codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter 'a' is modified at line 150]
-codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_pure_FP(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_pure_FP(int[],int),parameter 'a' is modified at line 142]
-codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter 'array' is modified at line 125]
-codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter 'array' is modified at line 118]
-codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter 'array' is modified at line 134,parameter 'array' is modified at line 132]
-codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable 'Test' is modified at line 15]
-codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter 'array' is modified at line 77]
-codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter 'this' is modified when calling `Test.set_impure(...)` at line 41,parameter 'this' is modified at line 19]
-codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global variable 'Test' is modified at line 23]
-codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter 'x' is modified at line 66]
-codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter 'test' is modified at line 56]
-codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter 'this' is modified at line 19]
-codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter 'array' is modified at line 71,parameter 'array' is modified at line 71,parameter 'array' is modified at line 72,parameter 'array' is modified at line 71]
+codetoanalyze/java/impurity/GlobalTest.java, GlobalTest$Foo.set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest$Foo.set_impure(),global variable `GlobalTest` accessed here,global variable `GlobalTest` modified here]
+codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.call_set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.call_set_impure(),global variable `GlobalTest` accessed here,when calling `void GlobalTest$Foo.set_impure()` here,global variable `GlobalTest` accessed here,global variable `GlobalTest` modified here]
+codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo),global variable `GlobalTest` accessed here,when calling `void GlobalTest.incr(GlobalTest$Foo,int)` here,parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),global variable `GlobalTest` modified here]
+codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo),global variable `GlobalTest` accessed here,assigned,when calling `void GlobalTest.incr(GlobalTest$Foo,int)` here,parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),global variable `GlobalTest` modified here]
+codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter `this` of void Localities$Counter.inc_impure(),parameter `this` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter `this` of void Localities$Foo.inc_impure(),parameter `this` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),parameter `a` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_pure_FP(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_pure_FP(int[],int),parameter `a` of boolean Localities.copy_ref_pure_FP(int[],int),parameter `a` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here]
+codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` accessed here,global variable `Test` modified here]
+codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here]
+codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter `this` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here]
+codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global variable `Test` accessed here,assigned,global variable `Test` modified here]
+codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter `x` of void Test.local_field_write_impure(Test),assigned,parameter `x` modified here]
+codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter `test` of void Test.parameter_field_write_impure(Test,boolean),parameter `test` modified here]
+codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter `this` of void Test.set_impure(int,int),parameter `this` modified here]
+codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter `array` of void Test.swap_impure(int[],int,int),parameter `array` modified here,parameter `array` of void Test.swap_impure(int[],int,int),parameter `array` modified here,parameter `array` of void Test.swap_impure(int[],int,int),parameter `array` modified here]
diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp
index 02b17e870..3acec4e7a 100644
--- a/infer/tests/codetoanalyze/objc/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp
@@ -1,2 +1,2 @@
-codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
-codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
+codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,invalid access occurs here]
+codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp
index 675be8a89..76d89f920 100644
--- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp
@@ -1,2 +1,2 @@
-codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest::deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,invalid access occurs here]
-codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,invalid access occurs here]
+codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest::deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
+codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]