diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml
index 0e7db7e62..bdd0f504c 100644
--- a/infer/src/IR/HilExp.ml
+++ b/infer/src/IR/HilExp.ml
@@ -237,6 +237,13 @@ module AccessExpression = struct
     aux init [] access_expr
 
 
+  let to_accesses access_expr =
+    let (), base, accesses =
+      to_accesses_fold access_expr ~init:() ~f_array_offset:(fun () index -> ((), index))
+    in
+    (base, accesses)
+
+
   let add_access access access_expr =
     match (access : _ Access.t) with
     | FieldAccess fld ->
@@ -249,6 +256,14 @@ module AccessExpression = struct
         address_of access_expr
 
 
+  let add_rev_accesses rev_accesses access_expr =
+    List.fold rev_accesses ~init:(Some access_expr) ~f:(fun access_expr_opt access ->
+        let open Option.Monad_infix in
+        access_expr_opt >>= add_access access )
+
+
+  let add_accesses accesses access_expr = add_rev_accesses (List.rev accesses) access_expr
+
   (** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *)
   let rec to_access_path t =
     let rec to_access_path_ t =
@@ -353,10 +368,14 @@ module AccessExpression = struct
         fold_vars_exp_opt exp_opt ~init ~f
 
 
-  let to_source_string access_expr =
+  let appears_in_source_code access_expr =
     (* should probably eventually check more than just the base but yolo *)
     let var, _ = get_base access_expr in
-    if Var.appears_in_source_code var then Some (F.asprintf "%a" pp access_expr) else None
+    Var.appears_in_source_code var
+
+
+  let to_source_string access_expr =
+    if appears_in_source_code access_expr then Some (F.asprintf "%a" pp access_expr) else None
 end
 
 let rec get_typ tenv = function
diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli
index 1bec37c9e..3628c185e 100644
--- a/infer/src/IR/HilExp.mli
+++ b/infer/src/IR/HilExp.mli
@@ -64,6 +64,8 @@ module AccessExpression : sig
     -> f_array_offset:('accum -> t option -> 'accum * 'array_index)
     -> 'accum * AccessPath.base * 'array_index Access.t list
 
+  val to_accesses : access_expression -> AccessPath.base * t option Access.t list
+
   val to_access_path : access_expression -> AccessPath.t
 
   val to_access_paths : access_expression list -> AccessPath.t list
@@ -93,6 +95,12 @@ module AccessExpression : sig
 
   val add_access : _ Access.t -> t -> t option
 
+  val add_accesses : _ Access.t list -> t -> t option
+
+  val add_rev_accesses : _ Access.t list -> t -> t option
+
+  val appears_in_source_code : t -> bool
+
   val to_source_string : t -> string option
   (** get a string representation of the access expression in terms of symbols that appear in the
      program, to show to the user *)
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index e6df1c7aa..f03c28ec8 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -54,7 +54,10 @@ module PulseTransferFunctions = struct
   let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc
       astate =
     (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *)
-    let crumb = ValueHistory.Assignment {lhs= lhs_access; location= loc} in
+    let crumb =
+      ValueHistory.Assignment
+        {lhs= PulseAbductiveDomain.explain_access_expr lhs_access astate; location= loc}
+    in
     match rhs_exp with
     | AccessExpression rhs_access -> (
         PulseOperations.read loc rhs_access astate
@@ -82,7 +85,12 @@ module PulseTransferFunctions = struct
     let read_all args astate =
       PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
     in
-    let crumb = ValueHistory.Call {f= `HilCall call; actuals; location= call_loc} in
+    let crumb =
+      ValueHistory.Call
+        { f= `HilCall call
+        ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
+        ; location= call_loc }
+    in
     let havoc_ret (ret, _) astate = PulseOperations.havoc_var [crumb] ret astate in
     let read_actuals_havoc_ret actuals ret astate = read_all actuals astate >>| havoc_ret ret in
     match call with
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index aa4f03599..0f744698e 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -85,6 +85,12 @@ let ( <= ) ~lhs ~rhs =
         ~rhs:(rhs.post :> PulseDomain.t)
 
 
+let explain_access_expr access_expr {post} =
+  PulseDomain.explain_access_expr access_expr (post :> base_domain)
+
+
+let explain_hil_exp hil_exp {post} = PulseDomain.explain_hil_exp hil_exp (post :> base_domain)
+
 module Stack = struct
   let is_abducible astate var =
     (* HACK: formals are pre-registered in the initial state *)
@@ -375,7 +381,9 @@ module PrePost = struct
         | Error invalidated_by ->
             Error
               (PulseDiagnostic.AccessToInvalidAddress
-                 {access= access_expr; invalidated_by; accessed_by= {action; history}})
+                 { access= explain_access_expr access_expr call_state.astate
+                 ; invalidated_by
+                 ; accessed_by= {action; history} })
         | Ok astate ->
             let call_state = {call_state with astate} in
             Container.fold_result
@@ -730,3 +738,6 @@ module PrePost = struct
         | Some astate_post ->
             Ok astate_post )
 end
+
+let explain_access_expr access_expr {post} =
+  PulseDomain.explain_access_expr access_expr (post :> base_domain)
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index b19dc7e7d..8ea31aee3 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -43,7 +43,7 @@ module Memory : sig
   val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
 
   val check_valid :
-       HilExp.AccessExpression.t PulseDomain.InterprocAction.t
+       HilExp.AccessExpression.t PulseDomain.explained PulseDomain.InterprocAction.t
     -> AbstractAddress.t
     -> t
     -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result
@@ -89,3 +89,8 @@ end
 val discard_unreachable : t -> t
 (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
     keep its size down *)
+
+val explain_access_expr :
+  HilExp.AccessExpression.t -> t -> HilExp.AccessExpression.t PulseDomain.explained
+
+val explain_hil_exp : HilExp.t -> t -> HilExp.t PulseDomain.explained
diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml
index 15b11d670..9626533cc 100644
--- a/infer/src/pulse/PulseDiagnostic.ml
+++ b/infer/src/pulse/PulseDiagnostic.ml
@@ -10,9 +10,9 @@ module F = Format
 
 type t =
   | AccessToInvalidAddress of
-      { access: HilExp.AccessExpression.t
+      { access: HilExp.AccessExpression.t PulseDomain.explained
       ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
-      ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t }
+      ; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t }
   | StackVariableAddressEscape of
       { variable: Var.t
       ; history: PulseDomain.ValueHistory.t
@@ -44,11 +44,13 @@ 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 invalidated f (trace : HilExp.AccessExpression.t PulseDomain.Trace.t) =
+      let pp_access_trace invalidated f
+          (trace : HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t) =
         match trace.action with
         | Immediate {imm= access; _} -> (
-          match HilExp.AccessExpression.to_source_string access with
-          | Some access_s when HilExp.AccessExpression.equal access invalidated ->
+          match HilExp.AccessExpression.to_source_string (access :> HilExp.AccessExpression.t) with
+          | Some access_s
+            when HilExp.AccessExpression.equal (access :> HilExp.AccessExpression.t) invalidated ->
               F.fprintf f "`%s` " access_s
           | Some access_s -> (
             match HilExp.AccessExpression.to_source_string invalidated with
@@ -101,7 +103,9 @@ let get_message = function
         line
       in
       let invalidation_line = line_of_trace invalidated_by in
-      F.asprintf "%a%a" (pp_access_trace access) accessed_by
+      F.asprintf "%a%a"
+        (pp_access_trace (access :> HilExp.AccessExpression.t))
+        accessed_by
         (pp_invalidation_trace invalidation_line)
         invalidated_by
   | StackVariableAddressEscape {variable; _} ->
@@ -119,7 +123,7 @@ let get_trace = function
           F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation )
         invalidated_by
       @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here"
-           (fun f (access : HilExp.AccessExpression.t) ->
+           (fun f (access : HilExp.AccessExpression.t PulseDomain.explained) ->
              F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp
                (access :> HilExp.AccessExpression.t) )
            accessed_by
diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli
index dc9343a4d..9992478e8 100644
--- a/infer/src/pulse/PulseDiagnostic.mli
+++ b/infer/src/pulse/PulseDiagnostic.mli
@@ -10,9 +10,9 @@ open! IStd
 (** an error to report to the user *)
 type t =
   | AccessToInvalidAddress of
-      { access: HilExp.AccessExpression.t
+      { access: HilExp.AccessExpression.t PulseDomain.explained
       ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
-      ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t }
+      ; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t }
   | StackVariableAddressEscape of
       { variable: Var.t
       ; history: PulseDomain.ValueHistory.t
diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml
index c28d8e44c..3c0ffc991 100644
--- a/infer/src/pulse/PulseDomain.ml
+++ b/infer/src/pulse/PulseDomain.ml
@@ -10,6 +10,8 @@ module L = Logging
 
 (* {2 Abstract domain description } *)
 
+type 'a explained = 'a [@@deriving compare]
+
 module Invalidation = struct
   type std_vector_function =
     | Assign
@@ -42,11 +44,11 @@ module Invalidation = struct
 
 
   type t =
-    | CFree of HilExp.AccessExpression.t
-    | CppDelete of HilExp.AccessExpression.t
+    | CFree of HilExp.AccessExpression.t explained
+    | CppDelete of HilExp.AccessExpression.t explained
     | GoneOutOfScope of Pvar.t * Typ.t
     | Nullptr
-    | StdVector of std_vector_function * HilExp.AccessExpression.t
+    | StdVector of std_vector_function * HilExp.AccessExpression.t explained
   [@@deriving compare]
 
   let issue_type_of_cause = function
@@ -100,14 +102,14 @@ module ValueHistory = struct
   type event =
     | VariableDeclaration of Location.t
     | CppTemporaryCreated of Location.t
-    | Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
+    | Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t}
     | Capture of
         { captured_as: AccessPath.base
-        ; captured: HilExp.AccessExpression.t
+        ; captured: HilExp.AccessExpression.t explained
         ; location: Location.t }
     | Call of
         { f: [`HilCall of HilInstr.call | `Model of string]
-        ; actuals: HilExp.t list
+        ; actuals: HilExp.t explained list
         ; location: Location.t }
   [@@deriving compare]
 
@@ -120,7 +122,8 @@ module ValueHistory = struct
         F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured
           AccessPath.pp_base captured_as
     | Assignment {lhs; location= _} ->
-        F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
+        if HilExp.AccessExpression.appears_in_source_code lhs then
+          F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
     | Call {f; actuals; location= _} ->
         let pp_f fmt = function
           | `HilCall call ->
@@ -236,7 +239,7 @@ end
 module Attribute = struct
   type t =
     | Invalid of Invalidation.t Trace.t
-    | MustBeValid of HilExp.AccessExpression.t InterprocAction.t
+    | MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
     | StdVectorReserve
@@ -784,3 +787,77 @@ let reachable_addresses astate =
     ~init:() ~finish:Fn.id
     ~f:(fun () _ _ _ -> Continue ())
   |> fst
+
+
+let rec evaluate_accesses address accesses astate =
+  match accesses with
+  | [] ->
+      Some address
+  | access :: next_accesses ->
+      let open Option.Monad_infix in
+      Memory.find_edge_opt address access astate.heap
+      >>= fun (addr, _) -> evaluate_accesses addr next_accesses astate
+
+
+let evaluate_access_path var should_deref astate =
+  let open Option.Monad_infix in
+  Stack.find_opt var astate.stack
+  >>= fun (addr_var, _) ->
+  if should_deref then evaluate_accesses addr_var [HilExp.Access.Dereference] astate
+  else Some addr_var
+
+
+let explain_address address astate =
+  GraphVisit.fold astate ~init:() ~var_filter:Var.appears_in_source_code
+    ~finish:(fun _ -> None)
+    ~f:(fun () address' var accesses ->
+      if AbstractAddress.equal address address' then Stop (Some (var, accesses)) else Continue ()
+      )
+  |> snd
+  |> Option.bind ~f:(fun (var, rev_accesses) ->
+         let base = HilExp.AccessExpression.address_of_base (var, Typ.void) in
+         HilExp.AccessExpression.add_rev_accesses rev_accesses base )
+
+
+let explain_access_expr access_expr astate =
+  if HilExp.AccessExpression.appears_in_source_code access_expr then access_expr
+  else
+    let (base_var, _), accesses = HilExp.AccessExpression.to_accesses access_expr in
+    let should_deref, accesses_left =
+      match accesses with [HilExp.Access.TakeAddress] -> (false, []) | _ -> (true, accesses)
+    in
+    match
+      let open Option.Monad_infix in
+      evaluate_access_path base_var should_deref astate
+      >>= fun base_address ->
+      explain_address base_address astate >>= HilExp.AccessExpression.add_accesses accesses_left
+    with
+    | Some explained ->
+        explained
+    | None ->
+        L.d_printfln "Can't explain how to reach address %a from state %a"
+          HilExp.AccessExpression.pp access_expr pp astate ;
+        access_expr
+
+
+let rec explain_hil_exp (e : HilExp.t) astate =
+  match e with
+  | AccessExpression access_expr ->
+      HilExp.AccessExpression (explain_access_expr access_expr astate)
+  | UnaryOperator (op, e', t) ->
+      HilExp.UnaryOperator (op, explain_hil_exp e' astate, t)
+  | BinaryOperator (op, e1, e2) ->
+      HilExp.BinaryOperator (op, explain_hil_exp e1 astate, explain_hil_exp e2 astate)
+  | Exception e' ->
+      HilExp.Exception (explain_hil_exp e' astate)
+  | Closure (proc_name, captured) ->
+      HilExp.Closure
+        (proc_name, List.map captured ~f:(fun (base, e') -> (base, explain_hil_exp e' astate)))
+  | Constant _ ->
+      e
+  | Cast (t, e') ->
+      HilExp.Cast (t, explain_hil_exp e' astate)
+  | Sizeof (t, Some e') ->
+      HilExp.Sizeof (t, Some (explain_hil_exp e' astate))
+  | Sizeof (_, None) ->
+      e
diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli
index 89bacd5a2..a1f14b4bb 100644
--- a/infer/src/pulse/PulseDomain.mli
+++ b/infer/src/pulse/PulseDomain.mli
@@ -8,6 +8,8 @@
 open! IStd
 module F = Format
 
+type 'a explained = private 'a
+
 module Invalidation : sig
   type std_vector_function =
     | Assign
@@ -23,11 +25,11 @@ module Invalidation : sig
   val pp_std_vector_function : Format.formatter -> std_vector_function -> unit
 
   type t =
-    | CFree of HilExp.AccessExpression.t
-    | CppDelete of HilExp.AccessExpression.t
+    | CFree of HilExp.AccessExpression.t explained
+    | CppDelete of HilExp.AccessExpression.t explained
     | GoneOutOfScope of Pvar.t * Typ.t
     | Nullptr
-    | StdVector of std_vector_function * HilExp.AccessExpression.t
+    | StdVector of std_vector_function * HilExp.AccessExpression.t explained
   [@@deriving compare]
 
   val issue_type_of_cause : t -> IssueType.t
@@ -39,14 +41,14 @@ module ValueHistory : sig
   type event =
     | VariableDeclaration of Location.t
     | CppTemporaryCreated of Location.t
-    | Assignment of {lhs: HilExp.access_expression; location: Location.t}
+    | Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t}
     | Capture of
         { captured_as: AccessPath.base
-        ; captured: HilExp.access_expression
+        ; captured: HilExp.AccessExpression.t explained
         ; location: Location.t }
     | Call of
         { f: [`HilCall of HilInstr.call | `Model of string]
-        ; actuals: HilExp.t list
+        ; actuals: HilExp.t explained list
         ; location: Location.t }
 
   type t = event list [@@deriving compare]
@@ -80,7 +82,7 @@ end
 module Attribute : sig
   type t =
     | Invalid of Invalidation.t Trace.t
-    | MustBeValid of HilExp.AccessExpression.t InterprocAction.t
+    | MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
     | StdVectorReserve
@@ -90,7 +92,7 @@ end
 module Attributes : sig
   include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t
 
-  val get_must_be_valid : t -> HilExp.AccessExpression.t InterprocAction.t option
+  val get_must_be_valid : t -> HilExp.AccessExpression.t explained InterprocAction.t option
 end
 
 module AbstractAddress : sig
@@ -192,3 +194,7 @@ type isograph_relation =
 val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation
 
 val is_isograph : lhs:t -> rhs:t -> mapping -> bool
+
+val explain_access_expr : HilExp.AccessExpression.t -> t -> HilExp.AccessExpression.t explained
+
+val explain_hil_exp : HilExp.t -> t -> HilExp.t explained
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 30ce94ea2..55ba35b46 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -27,7 +27,10 @@ module C = struct
     | [AccessExpression deleted_access] ->
         PulseOperations.invalidate
           (PulseDomain.InterprocAction.Immediate
-             {imm= PulseDomain.Invalidation.CFree deleted_access; location})
+             { imm=
+                 PulseDomain.Invalidation.CFree
+                   (PulseAbductiveDomain.explain_access_expr deleted_access astate)
+             ; location })
           location deleted_access astate
         >>| List.return
     | _ ->
@@ -43,7 +46,10 @@ module Cplusplus = struct
     | [AccessExpression deleted_access] ->
         PulseOperations.invalidate
           (PulseDomain.InterprocAction.Immediate
-             {imm= PulseDomain.Invalidation.CppDelete deleted_access; location})
+             { imm=
+                 PulseDomain.Invalidation.CppDelete
+                   (PulseAbductiveDomain.explain_access_expr deleted_access astate)
+             ; location })
           location deleted_access astate
         >>| List.return
     | _ ->
@@ -63,7 +69,10 @@ module Cplusplus = struct
         Ok astate )
     >>| fun astate ->
     [ PulseOperations.havoc_var
-        [PulseDomain.ValueHistory.Call {f= `Model "<lambda>"; actuals; location}]
+        [ PulseDomain.ValueHistory.Call
+            { f= `Model "<lambda>"
+            ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
+            ; location } ]
         ret_var astate ]
 
 
@@ -72,7 +81,12 @@ module Cplusplus = struct
     let read_all args astate =
       PulseOperations.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate
     in
-    let crumb = PulseDomain.ValueHistory.Call {f= `Model "<placement new>"; actuals; location} in
+    let crumb =
+      PulseDomain.ValueHistory.Call
+        { f= `Model "<placement new>"
+        ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
+        ; location }
+    in
     match List.rev actuals with
     | HilExp.AccessExpression expr :: other_actuals ->
         PulseOperations.read location expr astate
@@ -107,7 +121,10 @@ module StdVector = struct
     let array = deref_internal_array vector in
     let invalidation =
       PulseDomain.InterprocAction.Immediate
-        {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location}
+        { imm=
+            PulseDomain.Invalidation.StdVector
+              (vector_f, PulseAbductiveDomain.explain_access_expr vector astate)
+        ; location }
     in
     PulseOperations.invalidate_array_elements invalidation location array astate
     >>= PulseOperations.invalidate invalidation location array
@@ -123,7 +140,7 @@ module StdVector = struct
             { f=
                 `Model
                   (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f)
-            ; actuals
+            ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
             ; location }
         in
         reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
@@ -133,7 +150,12 @@ module StdVector = struct
 
   let at : model =
    fun location ~ret ~actuals astate ->
-    let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; actuals; location} in
+    let crumb =
+      PulseDomain.ValueHistory.Call
+        { f= `Model "std::vector::at"
+        ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
+        ; location }
+    in
     match actuals with
     | [AccessExpression vector_access_expr; index_exp] ->
         PulseOperations.read location
@@ -154,7 +176,10 @@ module StdVector = struct
     match actuals with
     | [AccessExpression vector; _value] ->
         let crumb =
-          PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; actuals; location}
+          PulseDomain.ValueHistory.Call
+            { f= `Model "std::vector::reserve"
+            ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
+            ; location }
         in
         reallocate_internal_array [crumb] vector Reserve location astate
         >>= PulseOperations.StdVector.mark_reserved location vector
@@ -168,7 +193,10 @@ module StdVector = struct
     match actuals with
     | [AccessExpression vector; _value] ->
         let crumb =
-          PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; actuals; location}
+          PulseDomain.ValueHistory.Call
+            { f= `Model "std::vector::push_back"
+            ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
+            ; location }
         in
         PulseOperations.StdVector.is_reserved location vector astate
         >>= fun (astate, is_reserved) ->
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index e9e668091..e622f5800 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -31,6 +31,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result
 let check_addr_access access action (address, history) astate =
   Memory.check_valid action address astate
   |> Result.map_error ~f:(fun invalidated_by ->
+         let access = PulseAbductiveDomain.explain_access_expr access astate in
          PulseDiagnostic.AccessToInvalidAddress
            {access; invalidated_by; accessed_by= {action; history}} )
 
@@ -139,7 +140,10 @@ and walk_access_expr ~on_last astate access_expr location =
       | [HilExp.Access.TakeAddress] ->
           Ok (astate, base_addr_trace)
       | _ ->
-          let action = InterprocAction.Immediate {imm= access_expr; location} in
+          let action =
+            InterprocAction.Immediate
+              {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location}
+          in
           walk
             (HilExp.AccessExpression.base base)
             ~dereference_to_ignore action ~on_last base_addr_trace
@@ -199,14 +203,18 @@ let write location access_expr addr astate =
 let invalidate cause location access_expr astate =
   materialize_address astate access_expr location
   >>= fun (astate, addr_trace) ->
-  check_addr_access access_expr (Immediate {imm= access_expr; location}) addr_trace astate
+  check_addr_access access_expr
+    (Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location})
+    addr_trace astate
   >>| mark_invalid cause addr_trace
 
 
 let invalidate_array_elements cause location access_expr astate =
   materialize_address astate access_expr location
   >>= fun (astate, addr_trace) ->
-  check_addr_access access_expr (Immediate {imm= access_expr; location}) addr_trace astate
+  check_addr_access access_expr
+    (Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location})
+    addr_trace astate
   >>| fun astate ->
   match Memory.find_opt (fst addr_trace) astate with
   | None ->
@@ -315,7 +323,10 @@ module Closures = struct
                 ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges
                 ~f:(fun (access, addr_trace) ->
                   if is_captured_fake_access access then
-                    check_addr_access lambda (Immediate {imm= lambda; location}) addr_trace astate
+                    check_addr_access lambda
+                      (Immediate
+                         {imm= PulseAbductiveDomain.explain_access_expr lambda astate; location})
+                      addr_trace astate
                     >>| fun _ -> ()
                   else Ok () )
           | _ ->
@@ -326,7 +337,9 @@ module Closures = struct
   let write location access_expr pname captured astate =
     let closure_addr = AbstractAddress.mk_fresh () in
     write location access_expr
-      (closure_addr, [ValueHistory.Assignment {lhs= access_expr; location}])
+      ( closure_addr
+      , [ ValueHistory.Assignment
+            {lhs= PulseAbductiveDomain.explain_access_expr access_expr astate; location} ] )
       astate
     >>| fun astate ->
     let fake_capture_edges = mk_capture_edges captured in
@@ -341,7 +354,11 @@ module Closures = struct
             read location access_expr astate
             >>= fun (astate, (address, trace)) ->
             let new_trace =
-              ValueHistory.Capture {captured_as; captured= captured_access_expr; location} :: trace
+              ValueHistory.Capture
+                { captured_as
+                ; captured= PulseAbductiveDomain.explain_access_expr captured_access_expr astate
+                ; location }
+              :: trace
             in
             Ok (astate, (address, new_trace) :: captured)
         | _ ->
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index bc91ee602..0a21e46ce 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,47 +1,47 @@
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `*n$0` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$6`,memory was invalidated by `delete` on `n$6` here,use-after-lifetime part of the trace starts here,assigned to `n$6`,invalid access to `n$6` 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,assigned to `n$0`,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$2`,when calling `templated_wrapper_access_ok` here,invalid access to `n$0->f` 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,assigned to `n$0`,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$2`,when calling `templated_wrapper_access_ok` here,invalid access to `n$0->f` 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 to `n$0`,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,assigned to `n$1`,when calling `deduplication::templated_access_function` here,invalid access to `n$0->f` 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 to `n$0`,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,assigned to `n$1`,when calling `deduplication::templated_access_function` here,invalid access to `n$0->f` 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,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `n$0` 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 to `n$5`,assigned to `y`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$4`,assigned to `z`,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` 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,assigned to `n$0`,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$0`,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `n$2`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `n$0`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,assigned to `n$0`,when calling `call_store()` here,when calling `store()` here,invalid access to `n$0->p` 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 to `n$13`,assigned to `result`,assigned to `n$9`,memory was invalidated by `delete` on `n$9` here,use-after-lifetime part of the trace starts here,assigned to `n$13`,assigned to `result`,assigned to `n$0`,invalid access to `*n$0` 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,assigned to `n$3`,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,assigned to `n$3`,assigned to `n$1->b`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,assigned to `n$0`,invalid access to `n$0->f` 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,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,returned from call to `getwrapperStack()`,invalid access to `n$0->f` 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` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `*ptr` 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` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `ptr` 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 `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `*(a.f)` 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 `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `*(a.f)` 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` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `*(a.f)` 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` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `*(a.f)` 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` on `this` here,use-after-lifetime part of the trace starts here,invalid access to `this` 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 to `y`,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,assigned to `z`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` 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` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` 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` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` 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` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` 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,returned from call to `__new(sizeof(Y))`,assigned to `y`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,when calling `call_store()` here,when calling `store()` here,invalid access to `*(y.p)` 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 to `result`,memory was invalidated by `delete` on `result` here,use-after-lifetime part of the trace starts here,assigned to `result`,invalid access to `*result` 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` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `*(*(&this.b))` here,use-after-lifetime part of the trace starts here,assigned to `*(this.b)`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access to `*(&rw.b->f)` 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,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,returned from call to `getwrapperStack()`,invalid access to `*(&rw.b->f)` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `n$0`,returned here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `n$1`,assigned to `y`,assigned to `n$0`,returned 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,invalid access to `n$2` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$3`,when calling `Simple` here,invalid access to `n$2->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$1`,memory was invalidated by `delete` on `n$1` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$8`,memory was invalidated by `delete` on `n$8` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$4`,when calling `Simple` here,invalid access to `n$2->f` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,invalid access to `n$2->f` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `n$3` 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 `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$4`,returned from call to `<placement new>(sizeof(use_after_destructor::S),n$4)`,assigned to `alias`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$4`,returned from call to `<placement new>(sizeof(use_after_destructor::S),n$4)`,assigned to `alias`,assigned to `n$0`,invalid access to `n$0->f` 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,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `n$7`,assigned to `alias`,assigned to `n$0`,invalid access to `n$0->f` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `n$3` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(int))`,assigned to `n$3->f`,returned from call to `use_after_destructor::S::S()`,assigned to `n$8`,invalid access to `*n$8` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `n$3` 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,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,invalid access to `n$0->f` 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,assigned to `n$0`,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` on `n$0` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `n$0` 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,assigned to `n$2`,memory was invalidated by call to `free()` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `n$0` 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,assigned to `n$2`,memory was invalidated by call to `free()` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `*n$0` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$10,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$9,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$11,(unsigned long) 1)`,assigned to `elt`,assigned to `n$9`,assigned to `y`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$10,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$21,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$21,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$12,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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()` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$9,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,returned here]
+codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `y`,returned 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `s` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,when calling `Simple` here,invalid access to `*(__param_0.f)` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `s` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,when calling `Simple` here,invalid access to `*(__param_0.f)` 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,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` 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 `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` 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 `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,memory was invalidated by `delete` on `alias` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalid access to `*(s.f)` 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,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalid access to `*(alias.f)` 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,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,memory was invalidated by `delete` on `alias` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalid access to `*(alias.f)` 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 `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` 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 `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(int))`,assigned to `*(this.f)`,returned from call to `use_after_destructor::S::S()`,invalid access to `*(*(&s.f))` 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 `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` 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,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,invalid access to `*(pc.f)` 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()` on `global_pointer` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `global_pointer` 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()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `x` 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()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `*x` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,invalid access to `*y` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` 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()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here]