[pulse] interprocedural histories and traces

Summary:
bigmacro_bender

There are 3 ways pulse tracks history. This is at least one too many. So
far, we have:

1. "histories": a humble list of "events" like "assigned here", "returned from call", ...

2. "interproc actions": a structured nesting of calls with a final "action", eg "f calls g calls h which does blah"

3. "traces", which combine one history with one interproc action

This diff gets rid of interproc actions and makes histories include
"nested" callee histories too. This allows pulse to track and display
how a value got assigned across function calls.

Traces are now more powerful and interleave histories and interproc
actions. This allows pulse to track how a value is fed into an action,
for instance performed in callee, which itself creates some more
(potentially now interprocedural) history before going to the next step
of the action (either another call or the action itself).

This gives much better traces, and some examples are added to showcase
this.

There are a lot of changes when applying summaries to keep track of
histories more accurately than was done before, but also a few
simplifications that give additional evidence that this is the right
concept.

Reviewed By: skcho

Differential Revision: D17908942

fbshipit-source-id: 3b62eaf78

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 =
+  let aux ~nesting errlog trace =
-    match action with
+    match trace with
-    | WrittenTo (PulseDomain.InterprocAction.Immediate {location}) ->
+    | WrittenTo access_trace ->
-        let rev_errlog =
+        PulseDomain.Trace.add_to_errlog ~nesting
-          Errlog.make_trace_element nesting location
+          (fun fmt () ->
-            (F.asprintf "%a '%a' is modified at %a" pp_param_source param_source Var.pp var
+            F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
-               Location.pp location)
+          access_trace errlog
-            []
+    | Invalid invalidation_trace ->
-          :: rev_errlog
+        PulseDomain.Trace.add_to_errlog ~nesting
-        in
+          (fun fmt invalid ->
-        List.rev_append rev_errlog errlog
+            F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
-    | WrittenTo (PulseDomain.InterprocAction.ViaCall {action; f; location}) ->
+              PulseDomain.Invalidation.describe invalid )
-        aux ~nesting:(nesting + 1)
+          invalidation_trace errlog
-          ( 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
   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)

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

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 =
+    let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
-      InterprocAction.Immediate {imm= Invalidation.GoneOutOfScope (pvar, typ); location= call_loc}
-    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_deref call_loc gone_out_of_scope out_of_scope_base astate
-    >>= PulseOperations.invalidate call_loc event out_of_scope_base
+    >>= 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)) ->
+          >>| fun (astate, rhs_addr_hist) -> PulseOperations.write_id lhs_id rhs_addr_hist astate
-          PulseOperations.write_id lhs_id (rhs_addr, rhs_history) astate
         in
         [check_error summary result]
     | Store {e1= lhs_exp; e2= rhs_exp; loc} ->

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
+            (* HACK: do not record the history of values in the pre as they are unused *)
-            let foot_heap =
+            let foot_stack = BaseStack.add var (addr, []) (astate.pre :> base_domain).stack in
-              BaseMemory.register_address (fst addr_hist) (astate.pre :> base_domain).heap
+            let foot_heap = BaseMemory.register_address addr (astate.pre :> base_domain).heap in
-            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_edge addr access new_addr_hist heap
-        |> BaseMemory.add_attribute addr
+        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history}))
-             (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc})) )
+    )
 
 
   let find_edge_opt address access astate =
     BaseMemory.find_edge_opt address access (astate.post :> base_domain).heap
 
 
-  let eval_edge addr access astate =
+  let eval_edge (addr_src, hist_src) access astate =
-    match find_edge_opt addr access astate with
+    match find_edge_opt addr_src access astate with
-    | Some addr_trace' ->
+    | Some addr_hist_dst ->
-        (astate, addr_trace')
+        (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
+          if BaseMemory.mem_edges addr_src (astate.pre :> base_domain).heap then
-            BaseMemory.add_edge addr access addr_trace' (astate.pre :> base_domain).heap
+            (* HACK: do not record the history of values in the pre as they are unused *)
-            |> BaseMemory.register_address (fst addr_trace')
+            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 =
+  let invalidate address invalidation location astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address action heap)
+    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
+        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history}))
-             (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc})) )
+    )
 
 
   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 ()
+           , (AbstractAddress.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) )
-             , [PulseDomain.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 =
+    let attr =
-      PulseDomain.InterprocAction.Immediate
+      Attribute.Invalid (Immediate {imm= GoneOutOfScope (pvar, typ); location; history})
-        {imm= PulseDomain.Invalidation.GoneOutOfScope (pvar, typ); location}
     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
+    ; subst: (AbstractAddress.t * ValueHistory.t) AddressMap.t
-          (** translation from callee addresses to caller addresses *)
+          (** 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 call_state, addr_hist_caller =
-              let astate, var_value = Stack.eval var call_state.astate in
+              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
+  let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre
-      history call_state =
+      ~addr_hist_caller call_state =
-    let mk_action action =
+    let add_call trace =
-      PulseDomain.InterprocAction.ViaCall
+      Trace.ViaCall
-        {action; f= Call callee_proc_name; location= call_location}
+        { in_call= trace
-    in
+        ; f= Call callee_proc_name
-    match visit call_state ~addr_callee:addr_pre ~addr_caller with
+        ; location= call_location
+        ; history= snd addr_hist_caller }
+    in
+    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 ->
+        >>| fun callee_access_trace ->
-        let action = mk_action callee_action in
+        let access_trace = add_call callee_access_trace in
-        match Memory.check_valid action addr_caller call_state.astate with
+        match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with
         | Error invalidated_by ->
             Error
-              (PulseDiagnostic.AccessToInvalidAddress
+              (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace})
-                 {invalidated_by; accessed_by= {action; history}})
         | 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, _) =
+                let astate, addr_hist_dest_caller =
-                  Memory.eval_edge addr_caller access call_state.astate
+                  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 (fst actual) ;
-    L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp addr_caller ;
     (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
+    fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state
-      ~f:(fun _var ~stack_value:(addr_pre, history) ~addr_caller 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
+        let addr_hist_fresh = (AbstractAddress.mk_fresh (), default_hist_caller) in
-        (addr_fresh, AddressMap.add addr_callee addr_fresh subst)
+        (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh)
-    | Some addr_caller ->
+    | Some addr_hist_caller ->
-        (addr_caller, subst)
+        (subst, addr_hist_caller)
 
 
-  let call_state_subst_find_or_new call_state addr_callee =
+  let call_state_subst_find_or_new call_state addr_callee ~default_hist_caller =
-    let addr_caller, new_subst = subst_find_or_new call_state.subst addr_callee in
+    let new_subst, addr_hist_caller =
-    if phys_equal new_subst call_state.subst then (call_state, addr_caller)
+      subst_find_or_new call_state.subst addr_callee ~default_hist_caller
-    else ({call_state with subst= new_subst}, addr_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=
+          (ViaCall
-              PulseDomain.InterprocAction.ViaCall
+             { f= Call proc_name
-                {action= trace.action; f= Call proc_name; location}
+             ; location= call_location
-          ; history= trace.history }
+             ; 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}
+            , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post}
-              :: 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) ->
+        >>= (fun (_edges, attrs) -> Attributes.get_written_to attrs)
-        Attributes.get_written_to attrs
+        |> fun written_to_callee_opt ->
-        >>| fun callee_action ->
+        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}))
+          (ViaCall
-        |> Option.value ~default:(Attribute.WrittenTo (Immediate {imm= (); location= call_loc}))
+             { 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 =
+      ~addr_hist_caller call_state =
-    L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ;
+    L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp (fst addr_hist_caller) ;
-    match visit call_state ~addr_callee ~addr_caller with
+    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
+              record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
-                ~cell_post call_state
+                ~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 ->
+            | Some return_caller_hist ->
-                return_caller
+                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
+      fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state
-        ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_caller 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 )

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
+       AbstractAddress.t * ValueHistory.t
-
+    -> Access.t
-  val check_valid :
+    -> PulseDomain.AddrTracePair.t
-       unit PulseDomain.InterprocAction.t
+    -> Location.t
-    -> AbstractAddress.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 :
+  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
-       AbstractAddress.t * PulseDomain.ValueHistory.t
-    -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.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
+  val eval_edge :
-  (** [eval_edge addr access astate] follows the edge [addr --access--> .] in memory and returns
+    AbstractAddress.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
-      what it points to or creates a fresh value if that edge didn't exist.  *)
+  (** [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
 

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
+  | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}
-      { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
+  | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
-      ; accessed_by: unit PulseDomain.Trace.t }
-  | StackVariableAddressEscape of
-      { variable: Var.t
-      ; history: PulseDomain.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) =
+      let pp_access_trace fmt (trace : unit Trace.t) =
-        match trace.action with
+        match trace with
-        | Immediate {imm= _; _} ->
+        | Immediate {imm= (); _} ->
             F.fprintf fmt "accessing memory that "
         | ViaCall {f; _} ->
-            F.fprintf fmt "call to %a eventually accesses memory that "
+            F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f
-              PulseDomain.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
       in
-      let line_of_trace trace =
+      let pp_invalidation_trace line fmt (trace : Invalidation.t Trace.t) =
-        let {Location.line; _} =
+        let pp_line fmt line = F.fprintf fmt " on line %d" line in
-          PulseDomain.InterprocAction.to_outer_location trace.PulseDomain.Trace.action
+        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 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"
+      let start_location = Trace.get_start_location invalidated_by in
-        (fun f invalidation ->
+      add_errlog_header ~title:"invalidation part of the trace starts here" start_location
-          F.fprintf f "memory %a here" PulseDomain.Invalidation.describe invalidation )
+      @@ Trace.add_to_errlog ~nesting:1
+           (fun fmt invalid -> F.fprintf fmt "%a" Invalidation.describe invalid)
            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 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
+      Trace.get_immediate invalidated_by |> Invalidation.issue_type_of_cause
-      |> PulseDomain.Invalidation.issue_type_of_cause
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape

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
+  | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}
-      { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
+  | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
-      ; accessed_by: unit PulseDomain.Trace.t }
-  | StackVariableAddressEscape of
-      { variable: Var.t
-      ; history: PulseDomain.ValueHistory.t
-      ; location: Location.t }
 
 val get_message : t -> string
 

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,104 +166,114 @@ module ValueHistory = struct
     | Capture {location}
     | CppTemporaryCreated location
     | FormalDeclared (_, location)
+    | VariableAccessed (_, location)
     | VariableDeclared (_, location) ->
         location
 
 
-  let pp_event fmt crumb =
+  let pp_event fmt event =
-    F.fprintf fmt "%a at %a" pp_event_no_location crumb Location.pp_line (location_of_event crumb)
+    F.fprintf fmt "%a at %a" pp_event_no_location event Location.pp_line (location_of_event event)
 
 
-  let errlog_trace_elem_of_event ~nesting crumb =
+  let pp fmt history =
-    let location = location_of_event crumb in
+    let rec pp_aux fmt = function
-    let description = F.asprintf "%a" pp_event_no_location crumb in
+      | [] ->
-    let tags = [] in
+          ()
-    Errlog.make_trace_element nesting location description tags
+      | (Call {f; in_call} as event) :: tail ->
-
+          F.fprintf fmt "%a@;" pp_event event ;
-
+          F.fprintf fmt "[%a]@;" pp_aux (List.rev in_call) ;
-  type t = event list [@@deriving compare]
+          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 =
+  let add_event_to_errlog ~nesting event errlog =
-    List.rev_map_append ~f:(errlog_trace_elem_of_event ~nesting) events 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}
+    | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t}
-    | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.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; _} ->
+    | ViaCall {in_call; _} ->
-        get_immediate action
+        get_immediate in_call
 
 
-  let pp pp_immediate fmt = function
+  let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location
-    | 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_history = function Immediate {history; _} | ViaCall {history; _} -> history
 
-  let to_outer_location = function Immediate {location} | ViaCall {location} -> location
+  let get_start_location trace =
-end
+    match get_history trace |> List.last with
+    | Some event ->
+        ValueHistory.location_of_event event
+    | None ->
+        get_outer_location trace
 
-module Trace = struct
-  type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
 
-  let pp pp_immediate f {action; history} =
+  let rec pp pp_immediate fmt = function
-    if Config.debug_level_analysis < 3 then InterprocAction.pp pp_immediate f action
+    | 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 f "{@[action=@[%a@]@;history=@[%a@]@]}" (InterprocAction.pp pp_immediate) action
+          F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp pp_immediate)
-        ValueHistory.pp history
+            in_call
-
+
-
+
-  let add_errlog_header ~title location errlog =
+  let rec add_to_errlog ~nesting pp_immediate trace errlog =
-    let depth = 0 in
+    match trace with
-    let tags = [] in
+    | Immediate {imm; location; history} ->
-    Errlog.make_trace_element depth location title tags :: errlog
+        ValueHistory.add_to_errlog ~nesting history
-
+        @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
-
+           :: errlog
-  let add_to_errlog ~header pp_immediate trace errlog =
+    | ViaCall {f; location; in_call; history} ->
-    let start_location =
+        ValueHistory.add_to_errlog ~nesting history
-      match ValueHistory.get_start_location trace.history with
+        @@ (fun errlog ->
-      | Some location ->
+             Errlog.make_trace_element nesting location
-          location
+               (F.asprintf "when calling %a here" CallEvent.pp f)
-      | None ->
+               []
-          InterprocAction.to_outer_location trace.action
+             :: errlog )
-    in
+        @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call
-    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
 end
 
@@ -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 =
+  let invalid_rank = Variants.to_rank (Invalid (Trace.mk_dummy Invalidation.Nullptr))
-    Variants.to_rank
-      (Invalid
-         {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []})
 
-
+  let must_be_valid_rank = Variants.to_rank (MustBeValid (Trace.mk_dummy ()))
-  let must_be_valid_rank = Variants.to_rank (MustBeValid InterprocAction.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)"
+        F.fprintf f "MustBeValid %a" (Trace.pp (pp_string_if_debug "access")) action
-          (InterprocAction.pp (fun _ () -> ()))
-          action Location.pp
-          (InterprocAction.to_outer_location action)
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
     | WrittenTo action ->
-        F.fprintf f "WrittenTo (written by %a @ %a)"
+        F.fprintf f "WrittenTo %a" (Trace.pp (pp_string_if_debug "mutation")) action
-          (InterprocAction.pp (fun _ () -> ()))
-          action Location.pp
-          (InterprocAction.to_outer_location 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 =
+  let invalidate (address, history) invalid location memory =
-    add_attribute address (Attribute.Invalid {action= invalidation; history}) memory
+    let invalidation = Trace.Immediate {imm= invalid; location; history} in
+    add_attribute address (Attribute.Invalid invalidation) memory
 
 
   let check_valid address memory =

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 :
+  val add_to_errlog : nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list
-    nesting:int -> event list -> 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}
+    | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t}
-    | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.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
+  val get_start_location : 'a t -> Location.t
-end
+  (** initial step in the history if not empty, or else same as {!get_outer_location} *)
 
-module Trace : sig
+  val get_immediate : 'a t -> 'a
-  type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
 
   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
 

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
+        PulseOperations.invalidate location PulseDomain.Invalidation.CFree deleted_access astate
-          (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CFree; location})
-          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
+        PulseOperations.invalidate location PulseDomain.Invalidation.CppDelete deleted_access
-          (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CppDelete; location})
+          astate
-          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, _), _) :: _ ->
+    | ((address, hist), _) :: _ ->
-        Ok [PulseOperations.write_id ret_id (address, [event]) astate]
+        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) ->
+        >>= fun (astate, (string_addr, string_hist)) ->
-        let invalidation =
+        let string_addr_hist = (string_addr, call_event :: string_hist) in
-          PulseDomain.InterprocAction.ViaCall
+        PulseOperations.invalidate_deref location CppDelete string_addr_hist astate
-            { 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 ->
-        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
+        PulseOperations.Closures.check_captured_addresses location lambda astate
-          (PulseDomain.InterprocAction.Immediate {imm= (); 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 =
+    PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate
-      PulseDomain.InterprocAction.Immediate
+    >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address
-        {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.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

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 =
+let check_addr_access location (address, history) astate =
-  Memory.check_valid action address 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 eval_access location addr_hist access astate =
-  let addr = fst addr_trace in
+  check_addr_access location addr_hist astate
-  let action = InterprocAction.Immediate {imm= (); location} in
+  >>| fun astate -> Memory.eval_edge addr_hist access astate
-  check_addr_access action addr_trace astate >>| fun astate -> Memory.eval_edge addr 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) ->
+        >>= fun (astate, addr_hist) ->
-        check_addr_access action addr_trace astate
+        check_addr_access location addr_hist astate
-        >>| fun astate -> Memory.eval_edge (fst addr_trace) (FieldAccess field) 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) ->
+        >>= fun (astate, addr_hist) ->
-        check_addr_access action addr_trace astate
+        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) ->
+  >>= fun (astate, addr_hist) ->
-  let action = InterprocAction.Immediate {imm= (); location} in
+  check_addr_access location addr_hist astate
-  check_addr_access action addr_trace astate
+  >>| fun astate -> Memory.eval_edge addr_hist Dereference astate
-  >>| fun astate -> Memory.eval_edge (fst addr_trace) 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 location addr_trace_ref astate
-  check_addr_access action addr_trace_ref astate
+  >>| Memory.add_edge addr_trace_ref access addr_trace_obj location
-  >>| Memory.add_edge (fst 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 location addr_trace astate >>| Memory.invalidate addr_trace cause location
-  check_addr_access action addr_trace astate >>| Memory.invalidate addr_trace cause
 
 
-let invalidate_deref location cause (addr_ref, history) astate =
+let invalidate_deref location cause ref_addr_hist astate =
-  let astate, (addr_obj, _) = Memory.eval_edge addr_ref Dereference astate in
+  let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist Dereference astate in
-  invalidate location cause (addr_obj, history) astate
+  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 location addr_trace astate
-  check_addr_access action 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 location addr_hist astate
-  check_addr_access action 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 ->
+            | Some (return_val, return_hist) ->
-                write_id (fst ret) (return_val, [event]) post
+                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]

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
+  Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result
-  -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-  -> PulseDomain.AddrTracePair.t
-  -> t
-  -> t access_result
 (** record that the address is invalid *)
 
 val invalidate_deref :
-     Location.t
+  Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result
-  -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-  -> PulseDomain.AddrTracePair.t
-  -> t
-  -> t access_result
 (** record that what the address points to is invalid *)
 
 val invalidate_array_elements :
-     Location.t
+  Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result
-  -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.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

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<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' 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` 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' is modified at line 33, column 3]
+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' is modified at line 15, column 3,parameter 'a' is modified at line 16, 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` 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' is modified at line 10, column 3,parameter 'a' is modified at line 9, column 3]
+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' 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, 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' is modified at line 40, column 60]
+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' is modified at line 44, column 3]
+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' 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, 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' 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, 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' is modified at line 12, column 37]
+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' is modified at line 33, column 22]
+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' is modified at line 10, column 41]
+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',was invalidated by `delete` 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, 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',was invalidated by call to `free()` 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',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' is modified at line 34, column 3]
+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' is modified at line 23, column 44]
+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' is modified at line 27, column 3]
+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' is modified at line 8, column 38]
+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' is modified at line 29, column 45]
+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' is modified at line 26, column 44]
+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' is modified at line 8, column 45]
+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' is modified at line 10, column 48]
+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' is modified at line 21, column 5]
+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]

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);
+}

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);
+}

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/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,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_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,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,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,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, 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,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, 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,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,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,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,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,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,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,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,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,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,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,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<_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,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/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/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/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/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/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/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/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, 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, 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, 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, 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_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_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_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, 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, 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/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/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/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/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/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/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/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/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/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/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_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, 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, 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, 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, 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, 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, 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, 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, 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, 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_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_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_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_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::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::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_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_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_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::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::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::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_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::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::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::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_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_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_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_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_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_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_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_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_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, 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, 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_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_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/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/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/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_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, 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, 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, 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, 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/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/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/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, 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, 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, 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, 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, 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, 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_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, 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, 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, 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_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, 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, 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, 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, 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, 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, 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, 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, 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/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]

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;
+}

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$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' 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.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' 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(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' is modified when calling `GlobalTest.incr(...)` at line 42,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` 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' 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` 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' is modified at line 67]
+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' is modified at line 57]
+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' is modified at line 150]
+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' is modified at line 142]
+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' is modified at line 125]
+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' is modified at line 118]
+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' is modified at line 134,parameter 'array' is modified at line 132]
+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' is modified at line 15]
+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' is modified at line 77]
+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' is modified when calling `Test.set_impure(...)` at line 41,parameter 'this' is modified at line 19]
+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' is modified at line 23]
+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' is modified at line 66]
+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' is modified at line 56]
+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' is modified at line 19]
+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' 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/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]

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, 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,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,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]

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, 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,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,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]