[pulse] more issue types and add details about why locations get invalidated

Summary: This is more flexible and allows us to give more details when reporting.

Reviewed By: mbouaziz

Differential Revision: D10509336

fbshipit-source-id: 79c3ac1c8

infer/src/base/IssueType.ml

@@ -389,6 +389,8 @@ let unreachable_code_after = from_string "UNREACHABLE_CODE"
 
 let unsafe_guarded_by_access = from_string "UNSAFE_GUARDED_BY_ACCESS"
 
+let use_after_delete = from_string "USE_AFTER_DELETE"
+
 let use_after_free = from_string "USE_AFTER_FREE"
 
 let use_after_lifetime = from_string "USE_AFTER_LIFETIME"

infer/src/base/IssueType.mli

@@ -291,6 +291,8 @@ val unreachable_code_after : t
 
 val unsafe_guarded_by_access : t
 
+val use_after_delete : t
+
 val use_after_free : t
 
 val use_after_lifetime : t

infer/src/checkers/Pulse.ml

@@ -46,7 +46,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Direct callee_pname when is_destructor callee_pname -> (
       match actuals with
       | [AccessExpression destroyed_access] ->
-          PulseDomain.invalidate call_loc destroyed_access astate
+          PulseDomain.invalidate
+            (CppDestructor (callee_pname, destroyed_access))
+            call_loc destroyed_access astate
       | _ ->
           Ok astate )
     | _ ->

infer/src/checkers/PulseDomain.ml

@@ -7,7 +7,7 @@
 open! IStd
 module F = Format
 module L = Logging
-open Result.Monad_infix
+module Invalidation = PulseInvalidation
 
 (* {2 Abstract domain description } *)
 
@@ -35,6 +35,8 @@ end = struct
   let pp = F.pp_print_int
 end
 
+(* {3 Heap domain } *)
+
 module Access = struct
   type t = AccessPath.access [@@deriving compare]
 
@@ -73,6 +75,8 @@ module Memory = struct
     Graph.find_opt addr memory >>= Edges.find_opt access
 end
 
+(* {3 Stack domain } *)
+
 (** to be used as maps values *)
 module AbstractAddressDomain_JoinIsMin : AbstractDomain.S with type astate = AbstractAddress.t =
 struct
@@ -93,48 +97,30 @@ end
    meaningless on their own. *)
 module AliasingDomain = AbstractDomain.Map (Var) (AbstractAddressDomain_JoinIsMin)
 
-type actor = {access_expr: AccessExpression.t; location: Location.t}
-
-let pp_actor f {access_expr; location} =
-  F.fprintf f "%a@%a" AccessExpression.pp access_expr Location.pp location
-
+(* {3 Invalid addresses domain } *)
 
-(** Locations known to be invalid for a reason described by an {!actor}. *)
-module type InvalidAddressesDomain = sig
+(** Locations known to be invalid for some reason *)
+module InvalidAddressesDomain : sig
   include AbstractDomain.S
 
   val empty : astate
 
-  val add : AbstractAddress.t -> actor -> astate -> astate
+  val add : AbstractAddress.t -> Invalidation.t -> astate -> astate
 
-  val get_invalidation : AbstractAddress.t -> astate -> actor option
-  (** return [Some actor] if the location was invalid by [actor], [None] if it is valid *)
+  val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option
+  (** None denotes a valid location *)
 
   val map : (AbstractAddress.t -> AbstractAddress.t) -> astate -> astate
   (** translate invalid addresses according to the mapping *)
-end
-
-module InvalidAddressesDomain : InvalidAddressesDomain = struct
-  module InvalidationReason = struct
-    type astate = actor
-
-    let join actor _ = actor
-
-    (* actors do not participate in the comparison of sets of invalid locations *)
-    let ( <= ) ~lhs:_ ~rhs:_ = true
-
-    let widen ~prev ~next:_ ~num_iters:_ = prev
-
-    let pp = pp_actor
-  end
+end = struct
+  include AbstractDomain.Map (AbstractAddress) (Invalidation)
 
-  include AbstractDomain.Map (AbstractAddress) (InvalidationReason)
+  let map f invalids = fold (fun key value map -> add (f key) value map) invalids empty
 
   let get_invalidation address invalids = find_opt address invalids
-
-  let map f invalids = fold (fun key actor invalids -> add (f key) actor invalids) invalids empty
 end
 
+(** the domain *)
 type t = {heap: Memory.t; stack: AliasingDomain.astate; invalids: InvalidAddressesDomain.astate}
 
 let initial =
@@ -169,7 +155,7 @@ module Domain : AbstractDomain.S with type astate = t = struct
 
       let compare_size _ _ = 0
 
-      let merge ~from ~to_ = to_ := Set.union !from !to_
+      let merge ~from ~to_ = if Config.debug_mode then to_ := Set.union !from !to_
 
       let pp f x = Set.pp f !x
     end
@@ -347,44 +333,49 @@ end
 
 (* {2 Access operations on the domain} *)
 
+type actor = {access_expr: AccessExpression.t; location: Location.t} [@@deriving compare]
+
 module Diagnostic = struct
   type t =
     | AccessToInvalidAddress of
-        { invalidated_at: actor
+        { invalidated_by: Invalidation.t
         ; accessed_by: actor
         ; address: AbstractAddress.t }
 
   let get_location (AccessToInvalidAddress {accessed_by= {location}}) = location
 
-  let get_message (AccessToInvalidAddress {accessed_by; invalidated_at; address}) =
+  let get_message (AccessToInvalidAddress {accessed_by; invalidated_by; address}) =
     let pp_debug_address f =
       if Config.debug_mode then F.fprintf f " (debug: %a)" AbstractAddress.pp address
     in
-    F.asprintf "`%a` accesses address `%a` past its lifetime%t" AccessExpression.pp
-      accessed_by.access_expr AccessExpression.pp invalidated_at.access_expr pp_debug_address
+    F.asprintf "`%a` accesses address %a past its lifetime%t" AccessExpression.pp
+      accessed_by.access_expr Invalidation.pp invalidated_by pp_debug_address
 
 
-  let get_trace (AccessToInvalidAddress {accessed_by; invalidated_at}) =
-    [ Errlog.make_trace_element 0 invalidated_at.location
-        (F.asprintf "invalidated `%a` here" AccessExpression.pp invalidated_at.access_expr)
+  let get_trace (AccessToInvalidAddress {accessed_by; invalidated_by}) =
+    [ Errlog.make_trace_element 0 invalidated_by.location
+        (F.asprintf "%a here" Invalidation.pp invalidated_by)
         []
     ; Errlog.make_trace_element 0 accessed_by.location
         (F.asprintf "accessed `%a` here" AccessExpression.pp accessed_by.access_expr)
         [] ]
 
 
-  let get_issue_type (AccessToInvalidAddress _) = IssueType.use_after_lifetime
+  let get_issue_type (AccessToInvalidAddress {invalidated_by= {cause}}) =
+    Invalidation.issue_type_of_cause cause
 end
 
 (** operations on the domain *)
 module Operations = struct
+  open Result.Monad_infix
+
   type 'a access_result = ('a, Diagnostic.t) result
 
   (** Check that the address is not known to be invalid *)
   let check_addr_access actor address astate =
     match InvalidAddressesDomain.get_invalidation address astate.invalids with
-    | Some invalidated_at ->
-        Error (Diagnostic.AccessToInvalidAddress {invalidated_at; accessed_by= actor; address})
+    | Some invalidated_by ->
+        Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address})
     | None ->
         Ok astate
 
@@ -477,11 +468,10 @@ module Operations = struct
 
   let havoc var astate = {astate with stack= AliasingDomain.remove var astate.stack}
 
-  let invalidate location access_expr astate =
+  let invalidate cause location access_expr astate =
     materialize_address astate access_expr location
     >>= fun (astate, addr) ->
-    let actor = {access_expr; location} in
-    check_addr_access actor addr astate >>| mark_invalid actor addr
+    check_addr_access {access_expr; location} addr astate >>| mark_invalid {cause; location} addr
 end
 
 include Domain

infer/src/checkers/PulseDomain.mli

@@ -41,4 +41,5 @@ val havoc : Var.t -> t -> t
 
 val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result
 
-val invalidate : Location.t -> AccessExpression.t -> t -> t access_result
+val invalidate :
+  PulseInvalidation.cause -> Location.t -> AccessExpression.t -> t -> t access_result

infer/src/checkers/PulseInvalidation.ml

@@ -0,0 +1,63 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+module L = Logging
+
+type cause =
+  | CppDelete of AccessExpression.t
+  | CppDestructor of Typ.Procname.t * AccessExpression.t
+  | StdVectorPushBack of AccessExpression.t
+[@@deriving compare]
+
+type t = {cause: cause; location: Location.t} [@@deriving compare]
+
+let issue_type_of_cause = function
+  | CppDelete _ ->
+      IssueType.use_after_delete
+  | CppDestructor _ ->
+      IssueType.use_after_lifetime
+  | StdVectorPushBack _ ->
+      IssueType.use_after_lifetime
+
+
+let pp f ({cause; location}[@warning "+9"]) =
+  match cause with
+  | CppDelete access_expr ->
+      F.fprintf f "invalidated by call to `delete %a` at %a" AccessExpression.pp access_expr
+        Location.pp location
+  | CppDestructor (proc_name, access_expr) ->
+      F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name
+        AccessExpression.pp access_expr Location.pp location
+  | StdVectorPushBack access_expr ->
+      F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a"
+        AccessExpression.pp access_expr Location.pp location
+
+
+module Domain : AbstractDomain.S with type astate = t = struct
+  type astate = t
+
+  let pp = pp
+
+  let join i1 i2 =
+    if [%compare.equal: t] i1 i2 then i1
+    else
+      (* take the max, but it should be unusual for the same location to be invalidated in two
+         different ways *)
+      let kept, forgotten = if compare i1 i2 >= 0 then (i1, i2) else (i2, i1) in
+      L.debug Analysis Quiet
+        "forgetting about invalidation %a for address already invalidated by %a@\n" pp forgotten pp
+        kept ;
+      kept
+
+
+  let ( <= ) ~lhs ~rhs = compare lhs rhs <= 0
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+end
+
+include Domain

infer/src/checkers/PulseInvalidation.mli

@@ -0,0 +1,19 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type cause =
+  | CppDelete of AccessExpression.t
+  | CppDestructor of Typ.Procname.t * AccessExpression.t
+  | StdVectorPushBack of AccessExpression.t
+[@@deriving compare]
+
+type t = {cause: cause; location: Location.t} [@@deriving compare]
+
+val issue_type_of_cause : cause -> IssueType.t
+
+include AbstractDomain.S with type astate = t

infer/src/checkers/PulseModels.ml

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

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

@@ -1,31 +1,31 @@
-codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign2_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a.str)` here]
-codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign3_ok, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a.a.str)` here]
-codetoanalyze/cpp/ownership/basics.cpp, aggregate_reassign_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `s.i` here]
-codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here]
-codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `ptr` here,accessed `*(ptr)` here]
-codetoanalyze/cpp/ownership/basics.cpp, pointer_arithmetic_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `a` here,accessed `a` here]
-codetoanalyze/cpp/ownership/basics.cpp, struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(a)` here,accessed `&(a)` here]
-codetoanalyze/cpp/ownership/returns.cpp, returns::FN_return_destructed_pointer_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `x` here,accessed `x` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `v.__internal_array[_]` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_throw_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_exit_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s->f` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `s->f` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing1_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `alias` here,accessed `s` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing2_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `s` here,accessed `alias` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, basic_placement_new_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `tptr` here,accessed `ptr` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, destructor_in_loop_ok, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, reinit_after_explicit_destructor_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `&(s)` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(s)` here,accessed `*(s.f)` here]
-codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(c)` here,accessed `pc->f` here]
-codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `result` here,accessed `*(result)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(x).__internal_array[_]` here,accessed `*(y)` here]
+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, 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]
+codetoanalyze/cpp/ownership/basics.cpp, struct_inside_loop_ok, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `A_~A(&(a))` at line 100, column 3 here,accessed `&(a)` here]
+codetoanalyze/cpp/ownership/returns.cpp, returns::FN_return_destructed_pointer_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `returns::S_~S(s)` at line 120, column 3 here,accessed `s` here]
+codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_ref_in_loop_ok, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 97, column 5 here,accessed `v.__internal_array[_]` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 112, column 5 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_throw_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 130, column 5 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_exit_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 121, column 5 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 37, column 3 here,accessed `s->f` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 103, column 3 here,accessed `s->f` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 133, column 3 here,accessed `s` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, FN_placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 141, column 3 here,accessed `alias` here]
+codetoanalyze/cpp/ownership/use_after_destructor.cpp, basic_placement_new_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(tptr)` at line 118, column 3 here,accessed `ptr` here]
+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_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/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]