[pulse] do not use access paths as they forget about &/*

Summary:
Now the domain can reason about `&` and `*` too. When recording `&`
between two locations also record a back-edge `*`, and vice-versa.

Reviewed By: mbouaziz

Differential Revision: D10509335

fbshipit-source-id: 8091b6ec0

infer/src/IR/AccessExpression.ml

@@ -20,6 +20,68 @@ type t =
   | Dereference of t
 [@@deriving compare]
 
+let may_pp_typ fmt typ =
+  if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ
+
+
+let rec pp fmt = function
+  | Base (pvar, typ) ->
+      Var.pp fmt pvar ; may_pp_typ fmt typ
+  | FieldOffset (Dereference ae, fld) ->
+      F.fprintf fmt "%a->%a" pp ae Typ.Fieldname.pp fld
+  | FieldOffset (ae, fld) ->
+      F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld
+  | ArrayOffset (ae, typ, []) ->
+      F.fprintf fmt "%a[_]%a" pp ae may_pp_typ typ
+  | ArrayOffset (ae, typ, index_aes) ->
+      F.fprintf fmt "%a[%a]%a" pp ae
+        (PrettyPrintable.pp_collection ~pp_item:pp)
+        index_aes may_pp_typ typ
+  | AddressOf ae ->
+      F.fprintf fmt "&(%a)" pp ae
+  | Dereference ae ->
+      F.fprintf fmt "*(%a)" pp ae
+
+
+module Access = struct
+  type access_expr = t [@@deriving compare]
+
+  type t =
+    | FieldAccess of Typ.Fieldname.t
+    | ArrayAccess of typ_ * access_expr list
+    | TakeAddress
+    | Dereference
+  [@@deriving compare]
+
+  let pp fmt = function
+    | FieldAccess field_name ->
+        Typ.Fieldname.pp fmt field_name
+    | ArrayAccess (_, []) ->
+        F.pp_print_string fmt "[_]"
+    | ArrayAccess (_, index_aps) ->
+        F.fprintf fmt "[%a]" (PrettyPrintable.pp_collection ~pp_item:pp) index_aps
+    | TakeAddress ->
+        F.pp_print_string fmt "&"
+    | Dereference ->
+        F.pp_print_string fmt "*"
+end
+
+let to_accesses ae =
+  let rec aux accesses = function
+    | Base base ->
+        (base, accesses)
+    | FieldOffset (ae, fld) ->
+        aux (Access.FieldAccess fld :: accesses) ae
+    | ArrayOffset (ae, typ, index_aes) ->
+        aux (Access.ArrayAccess (typ, index_aes) :: accesses) ae
+    | AddressOf ae ->
+        aux (Access.TakeAddress :: accesses) ae
+    | Dereference ae ->
+        aux (Access.Dereference :: accesses) ae
+  in
+  aux [] ae
+
+
 (** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *)
 let rec to_access_path t =
   let rec to_access_path_ t =
@@ -96,29 +158,6 @@ let rec get_typ t tenv : Typ.t option =
       match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None )
 
 
-let may_pp_typ fmt typ =
-  if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ
-
-
-let rec pp fmt = function
-  | Base (pvar, typ) ->
-      Var.pp fmt pvar ; may_pp_typ fmt typ
-  | FieldOffset (Dereference ae, fld) ->
-      F.fprintf fmt "%a->%a" pp ae Typ.Fieldname.pp fld
-  | FieldOffset (ae, fld) ->
-      F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld
-  | ArrayOffset (ae, typ, []) ->
-      F.fprintf fmt "%a[_]%a" pp ae may_pp_typ typ
-  | ArrayOffset (ae, typ, index_aes) ->
-      F.fprintf fmt "%a[%a]%a" pp ae
-        (PrettyPrintable.pp_collection ~pp_item:pp)
-        index_aes may_pp_typ typ
-  | AddressOf ae ->
-      F.fprintf fmt "&(%a)" pp ae
-  | Dereference ae ->
-      F.fprintf fmt "*(%a)" pp ae
-
-
 let equal = [%compare.equal: t]
 
 let base_of_id id typ = (Var.of_id id, typ)

infer/src/IR/AccessExpression.mli

@@ -19,6 +19,21 @@ type t =
   (* dereference operator * *)
 [@@deriving compare]
 
+module Access : sig
+  type access_expr = t [@@deriving compare]
+
+  type t =
+    | FieldAccess of Typ.Fieldname.t
+    | ArrayAccess of Typ.t * access_expr list
+    | TakeAddress
+    | Dereference
+  [@@deriving compare]
+
+  val pp : Format.formatter -> t -> unit
+end
+
+val to_accesses : t -> AccessPath.base * Access.t list
+
 val to_access_path : t -> AccessPath.t
 
 val to_access_paths : t list -> AccessPath.t list

infer/src/checkers/Pulse.ml

@@ -47,7 +47,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       match actuals with
       | [AccessExpression destroyed_access] ->
           PulseDomain.invalidate
-            (CppDestructor (callee_pname, destroyed_access))
+            (CppDestructor (callee_pname, destroyed_access, call_loc))
             call_loc destroyed_access astate
       | _ ->
           Ok astate )
@@ -80,9 +80,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           match rhs_exp with
           | AccessExpression rhs_access ->
               PulseDomain.read loc rhs_access astate
+          | Constant (Cint address) when IntLit.iszero address ->
+              Ok (astate, PulseDomain.AbstractAddress.nullptr)
           | _ ->
               PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate
-              >>= fun astate -> Ok (astate, PulseDomain.AbstractAddress.mk_fresh ())
+              >>= fun astate ->
+              Ok
+                ( astate
+                , (* TODO: we could avoid creating and recording a fresh location whenever
+                       [lhs_access] is not already present in the state so that we keep its
+                       evaluation lazy, which would have the same semantic result but won't make the
+                       state grow needlessly in case we never need that value again. We would just
+                       need to add a function {!PulseDomain.freshen access_expr} that does the lazy
+                       refreshing and use it instead of {!PulseDomain.write} below in this case. *)
+                  PulseDomain.AbstractAddress.mk_fresh () )
         in
         Result.bind rhs_result ~f:(fun (astate, rhs_value) ->
             PulseDomain.write loc lhs_access rhs_value astate )

infer/src/checkers/PulseDomain.ml

@@ -15,6 +15,8 @@ module Invalidation = PulseInvalidation
 module AbstractAddress : sig
   type t = private int [@@deriving compare]
 
+  val nullptr : t
+
   val equal : t -> t -> bool
 
   val mk_fresh : unit -> t
@@ -25,7 +27,10 @@ end = struct
 
   let equal = [%compare.equal: t]
 
-  let next_fresh = ref 0
+  (** distinguish 0 since it's always an invalid address *)
+  let nullptr = 0
+
+  let next_fresh = ref 1
 
   let mk_fresh () =
     let l = !next_fresh in
@@ -37,14 +42,35 @@ end
 
 (* {3 Heap domain } *)
 
-module Access = struct
-  type t = AccessPath.access [@@deriving compare]
+module Memory : sig
+  module Edges : module type of PrettyPrintable.MakePPMap (AccessExpression.Access)
 
-  let pp = AccessPath.pp_access
-end
+  type edges = AbstractAddress.t Edges.t
+
+  type t
+
+  val empty : t
+
+  val find_opt : AbstractAddress.t -> t -> edges option
+
+  val for_all : (AbstractAddress.t -> edges -> bool) -> t -> bool
+
+  val fold : (AbstractAddress.t -> edges -> 'accum -> 'accum) -> t -> 'accum -> 'accum
+
+  val pp : F.formatter -> t -> unit
+
+  val add_edge : AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddress.t -> t -> t
+
+  val add_edge_and_back_edge :
+    AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddress.t -> t -> t
+
+  val find_edge_opt :
+    AbstractAddress.t -> AccessExpression.Access.t -> t -> AbstractAddress.t option
+end = struct
+  module Edges = PrettyPrintable.MakePPMap (AccessExpression.Access)
+
+  type edges = AbstractAddress.t Edges.t
 
-module Memory = struct
-  module Edges = PrettyPrintable.MakePPMap (Access)
   module Graph = PrettyPrintable.MakePPMap (AbstractAddress)
 
   (* {3 Monomorphic {!PPMap} interface as needed } *)
@@ -70,6 +96,19 @@ module Memory = struct
     Graph.add addr_src (Edges.add access addr_end edges) memory
 
 
+  (** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because
+      [*(&x) = &( *x ) = x]. *)
+  let add_edge_and_back_edge addr_src (access : AccessExpression.Access.t) addr_end memory =
+    let memory = add_edge addr_src access addr_end memory in
+    match access with
+    | ArrayAccess _ | FieldAccess _ ->
+        memory
+    | TakeAddress ->
+        add_edge addr_end Dereference addr_src memory
+    | Dereference ->
+        add_edge addr_end TakeAddress addr_src memory
+
+
   let find_edge_opt addr access memory =
     let open Option.Monad_infix in
     Graph.find_opt addr memory >>= Edges.find_opt access
@@ -124,7 +163,14 @@ end
 type t = {heap: Memory.t; stack: AliasingDomain.astate; invalids: InvalidAddressesDomain.astate}
 
 let initial =
-  {heap= Memory.empty; stack= AliasingDomain.empty; invalids= InvalidAddressesDomain.empty}
+  { heap= Memory.empty
+  ; stack= AliasingDomain.empty
+  ; invalids=
+      InvalidAddressesDomain.empty
+      (* TODO: this makes the analysis go a bit overboard with the Nullptr reports. *)
+      (* (\* always recall that 0 is invalid *\)
+         InvalidAddressesDomain.add AbstractAddress.nullptr Nullptr InvalidAddressesDomain.empty *)
+  }
 
 
 module Domain : AbstractDomain.S with type astate = t = struct
@@ -357,16 +403,22 @@ module Diagnostic = struct
 
 
   let get_trace (AccessToInvalidAddress {accessed_by; invalidated_by}) =
-    [ Errlog.make_trace_element 0 invalidated_by.location
+    let invalidated_by_trace =
+      Invalidation.get_location invalidated_by
+      |> Option.map ~f:(fun location ->
+             Errlog.make_trace_element 0 location
                (F.asprintf "%a here" Invalidation.pp invalidated_by)
-        []
-    ; Errlog.make_trace_element 0 accessed_by.location
+               [] )
+      |> Option.to_list
+    in
+    invalidated_by_trace
+    @ [ Errlog.make_trace_element 0 accessed_by.location
           (F.asprintf "accessed `%a` here" AccessExpression.pp accessed_by.access_expr)
           [] ]
 
 
-  let get_issue_type (AccessToInvalidAddress {invalidated_by= {cause}}) =
-    Invalidation.issue_type_of_cause cause
+  let get_issue_type (AccessToInvalidAddress {invalidated_by}) =
+    Invalidation.issue_type_of_cause invalidated_by
 end
 
 (** operations on the domain *)
@@ -397,7 +449,7 @@ module Operations = struct
     | [a], Some new_addr ->
         check_addr_access actor addr astate
         >>| fun astate ->
-        let heap = Memory.add_edge addr a new_addr astate.heap in
+        let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in
         ({astate with heap}, new_addr)
     | a :: path, _ -> (
         check_addr_access actor addr astate
@@ -405,7 +457,7 @@ module Operations = struct
         match Memory.find_edge_opt addr a astate.heap with
         | None ->
             let addr' = AbstractAddress.mk_fresh () in
-            let heap = Memory.add_edge addr a addr' astate.heap in
+            let heap = Memory.add_edge_and_back_edge addr a addr' astate.heap in
             let astate = {astate with heap} in
             walk actor ~overwrite_last addr' path astate
         | Some addr' ->
@@ -414,7 +466,12 @@ module Operations = struct
 
   (** add addresses to the state to give a address to the destination of the given access path *)
   let walk_access_expr ?overwrite_last astate access_expr location =
-    let (access_var, _), access_list = AccessExpression.to_access_path access_expr in
+    let (access_var, _), access_list = AccessExpression.to_accesses access_expr in
+    if Config.write_html then
+      L.d_strln
+        (F.asprintf "Accessing %a -> [%a]" Var.pp access_var
+           (Pp.seq ~sep:"," AccessExpression.Access.pp)
+           access_list) ;
     match (overwrite_last, access_list) with
     | Some new_addr, [] ->
         let stack = AliasingDomain.add access_var new_addr astate.stack in
@@ -475,7 +532,7 @@ module Operations = struct
   let invalidate cause location access_expr astate =
     materialize_address astate access_expr location
     >>= fun (astate, addr) ->
-    check_addr_access {access_expr; location} addr astate >>| mark_invalid {cause; location} addr
+    check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr
 end
 
 include Domain

infer/src/checkers/PulseDomain.mli

@@ -10,6 +10,8 @@ open! IStd
 module AbstractAddress : sig
   type t = private int [@@deriving compare]
 
+  val nullptr : t
+
   val mk_fresh : unit -> t
 end
 
@@ -41,5 +43,4 @@ val havoc : Var.t -> t -> t
 
 val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result
 
-val invalidate :
-  PulseInvalidation.cause -> Location.t -> AccessExpression.t -> t -> t access_result
+val invalidate : PulseInvalidation.t -> Location.t -> AccessExpression.t -> t -> t access_result

infer/src/checkers/PulseInvalidation.ml

@@ -8,38 +8,50 @@ open! IStd
 module F = Format
 module L = Logging
 
-type cause =
-  | CppDelete of AccessExpression.t
-  | CppDestructor of Typ.Procname.t * AccessExpression.t
-  | CFree of AccessExpression.t
-  | StdVectorPushBack of AccessExpression.t
+type t =
+  | CFree of AccessExpression.t * Location.t
+  | CppDelete of AccessExpression.t * Location.t
+  | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t
+  | Nullptr
+  | StdVectorPushBack of AccessExpression.t * Location.t
 [@@deriving compare]
 
-type t = {cause: cause; location: Location.t} [@@deriving compare]
-
 let issue_type_of_cause = function
+  | CFree _ ->
+      IssueType.use_after_free
   | CppDelete _ ->
       IssueType.use_after_delete
   | CppDestructor _ ->
       IssueType.use_after_lifetime
-  | CFree _ ->
-      IssueType.use_after_free
+  | Nullptr ->
+      IssueType.null_dereference
   | StdVectorPushBack _ ->
       IssueType.use_after_lifetime
 
 
-let pp f ({cause; location}[@warning "+9"]) =
-  match cause with
-  | CppDelete access_expr ->
+let get_location = function
+  | CFree (_, location)
+  | CppDelete (_, location)
+  | CppDestructor (_, _, location)
+  | StdVectorPushBack (_, location) ->
+      Some location
+  | Nullptr ->
+      None
+
+
+let pp f = function
+  | CFree (access_expr, location) ->
+      F.fprintf f "invalidated by call to `free(%a)` at %a" AccessExpression.pp access_expr
+        Location.pp location
+  | CppDelete (access_expr, location) ->
       F.fprintf f "invalidated by call to `delete %a` at %a" AccessExpression.pp access_expr
         Location.pp location
-  | CppDestructor (proc_name, access_expr) ->
+  | CppDestructor (proc_name, access_expr, location) ->
       F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name
         AccessExpression.pp access_expr Location.pp location
-  | CFree access_expr ->
-      F.fprintf f "invalidated by call to `free(%a)` at %a" AccessExpression.pp access_expr
-        Location.pp location
-  | StdVectorPushBack access_expr ->
+  | Nullptr ->
+      F.fprintf f "null pointer"
+  | StdVectorPushBack (access_expr, location) ->
       F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a"
         AccessExpression.pp access_expr Location.pp location
 

infer/src/checkers/PulseInvalidation.mli

@@ -6,15 +6,15 @@
  *)
 open! IStd
 
-type cause =
-  | CppDelete of AccessExpression.t
-  | CppDestructor of Typ.Procname.t * AccessExpression.t
-  | CFree of AccessExpression.t
-  | StdVectorPushBack of AccessExpression.t
-[@@deriving compare]
+type t =
+  | CFree of AccessExpression.t * Location.t
+  | CppDelete of AccessExpression.t * Location.t
+  | CppDestructor of Typ.Procname.t * AccessExpression.t * Location.t
+  | Nullptr
+  | StdVectorPushBack of AccessExpression.t * Location.t
 
-type t = {cause: cause; location: Location.t} [@@deriving compare]
+val issue_type_of_cause : t -> IssueType.t
 
-val issue_type_of_cause : cause -> IssueType.t
+val get_location : t -> Location.t option
 
 include AbstractDomain.S with type astate = t

infer/src/checkers/PulseModels.ml

@@ -21,7 +21,7 @@ module C = struct
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression deleted_access] ->
-        PulseDomain.invalidate (CFree deleted_access) location deleted_access astate
+        PulseDomain.invalidate (CFree (deleted_access, location)) location deleted_access astate
     | _ ->
         Ok astate
 end
@@ -33,7 +33,9 @@ module Cplusplus = struct
     >>= fun astate ->
     match actuals with
     | [AccessExpression deleted_access] ->
-        PulseDomain.invalidate (CppDelete deleted_access) location deleted_access astate
+        PulseDomain.invalidate
+          (CppDelete (deleted_access, location))
+          location deleted_access astate
     | _ ->
         Ok astate
 
@@ -82,8 +84,9 @@ module StdVector = struct
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        PulseDomain.invalidate (StdVectorPushBack vector) location (deref_internal_array vector)
-          astate
+        PulseDomain.invalidate
+          (StdVectorPushBack (vector, location))
+          location (deref_internal_array vector) astate
     | _ ->
         Ok astate
 end

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,6 +1,6 @@
-codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(&(a))` at line 39, column 3 here,accessed `&(a.str)` here]
-codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(&(a))` at line 53, column 3 here,accessed `&(a.a.str)` here]
-codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(&(s))` at line 25, column 3 here,accessed `s.i` here]
+codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign2_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `AggregateWithConstructedField_~AggregateWithConstructedField(&(a))` at line 39, column 3 here,accessed `&(a)` here]
+codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign3_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `NestedAggregate_~NestedAggregate(&(a))` at line 53, column 3 here,accessed `&(a)` here]
+codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign_ok, 7, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(&(s))` at line 25, column 3 here,accessed `&(s)` here]
 codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60, column 5 here,accessed `*(ptr)` here]
 codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` here]
 codetoanalyze/cpp/ownership/basics.cpp, pointer_arithmetic_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `Aggregate_~Aggregate(a)` at line 77, column 3 here,accessed `a` here]
@@ -25,8 +25,9 @@ codetoanalyze/cpp/ownership/use_after_destructor.cpp, basic_placement_new_ok, 4,
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 163, column 3 here,accessed `&(s)` here]
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 54, column 3 here,accessed `&(s)` here]
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 34, column 3 here,accessed `&(s)` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 61, column 3 here,accessed `*(s.f)` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 61, column 3 here,accessed `&(s)` here]
 codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 186, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(x), ..)` at line 13, column 3 here,accessed `*(y)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(x), ..)` at line 19, column 3 here,accessed `*(y)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(x, ..)` at line 12, column 3 here,accessed `*(y)` here]

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -7,9 +7,15 @@
 #include <iostream>
 #include <vector>
 
-void deref_vector_element_after_lifetime_bad() {
+void deref_vector_element_after_lifetime_bad(std::vector<int>& x) {
+  int* y = &x[1];
+  x.push_back(42);
+  std::cout << *y << "\n";
+}
+
+void deref_local_vector_element_after_lifetime_bad() {
   std::vector<int> x = {0, 0};
   int* y = &x[1];
-  x.push_back(4);
+  x.push_back(42);
   std::cout << *y << "\n";
 }