From 38ced865f3695966d528ad9503cd3cb66fc68b56 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 26 Oct 2018 07:30:11 -0700 Subject: [PATCH] [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 | 2 + infer/src/base/IssueType.mli | 2 + infer/src/checkers/Pulse.ml | 4 +- infer/src/checkers/PulseDomain.ml | 76 ++++++++----------- infer/src/checkers/PulseDomain.mli | 3 +- infer/src/checkers/PulseInvalidation.ml | 63 +++++++++++++++ infer/src/checkers/PulseInvalidation.mli | 19 +++++ infer/src/checkers/PulseModels.ml | 5 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 62 +++++++-------- 9 files changed, 158 insertions(+), 78 deletions(-) create mode 100644 infer/src/checkers/PulseInvalidation.ml create mode 100644 infer/src/checkers/PulseInvalidation.mli diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 28e5ecd43..3a4d70649 100644 --- a/infer/src/base/IssueType.ml +++ b/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" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 7f4ade9bf..f5c6ad5dd 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 440306b8b..5b7391894 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 ) | _ -> diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 93d5efa0e..9e5cff411 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index a10c5b868..65d7d4fa6 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/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 diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml new file mode 100644 index 000000000..7147e441f --- /dev/null +++ b/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 diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli new file mode 100644 index 000000000..e0bd169b4 --- /dev/null +++ b/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 diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index a668dcdd1..f83b526fb 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index a92708382..1d640f60c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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]