diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index a67646f1d..5bb1f4454 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -8,13 +8,17 @@ open! IStd module F = Format open Result.Monad_infix -let check_error summary loc = function +let report summary diagnostic = + let open PulseDomain.Diagnostic in + Reporting.log_error summary ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic) + (get_issue_type diagnostic) (get_message diagnostic) + + +let check_error summary = function | Ok astate -> astate | Error (astate, diagnostic) -> - let message = PulseDomain.Diagnostic.to_string diagnostic in - Reporting.log_error summary ~loc IssueType.use_after_lifetime message ; - astate + report summary diagnostic ; astate module TransferFunctions (CFG : ProcCfg.S) = struct @@ -23,7 +27,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = Summary.t - let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags _call_loc astate = + let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate = let model = match call with | Indirect _ -> @@ -32,31 +36,31 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Direct callee_pname -> PulseModels.dispatch callee_pname in - match model with None -> Ok astate | Some model -> model ~ret ~actuals astate + match model with None -> Ok astate | Some model -> model call_loc ~ret ~actuals astate let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t) = match instr with | Assign (lhs_access, rhs_exp, loc) -> - (* try to evaluate [rhs_exp] down to an abstract location or generate a fresh one *) + (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) let rhs_result = match rhs_exp with | AccessExpression rhs_access -> - PulseDomain.read rhs_access astate + PulseDomain.read loc rhs_access astate | _ -> - PulseDomain.read_all (HilExp.get_access_exprs rhs_exp) astate - >>= fun astate -> Ok (astate, PulseDomain.AbstractLocation.mk_fresh ()) + PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate + >>= fun astate -> Ok (astate, PulseDomain.AbstractAddress.mk_fresh ()) in Result.bind rhs_result ~f:(fun (astate, rhs_value) -> - PulseDomain.write lhs_access rhs_value astate ) - |> check_error summary loc + PulseDomain.write loc lhs_access rhs_value astate ) + |> check_error summary | Assume (condition, _, _, loc) -> - PulseDomain.read_all (HilExp.get_access_exprs condition) astate |> check_error summary loc + PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary | Call (ret, call, actuals, flags, loc) -> - PulseDomain.read_all (List.concat_map actuals ~f:HilExp.get_access_exprs) astate + PulseDomain.read_all loc (List.concat_map actuals ~f:HilExp.get_access_exprs) astate >>= dispatch_call ret call actuals flags loc - |> check_error summary loc + |> check_error summary let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index c3e9d3736..b3f23e84f 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -10,7 +10,7 @@ module L = Logging open Result.Monad_infix (** An abstract address in memory. *) -module AbstractLocation : sig +module AbstractAddress : sig type t = private int [@@deriving compare] val equal : t -> t -> bool @@ -33,18 +33,18 @@ end = struct let pp = F.pp_print_int end -module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLocation.t = struct - type astate = AbstractLocation.t +module AbstractAddressDomain : AbstractDomain.S with type astate = AbstractAddress.t = struct + type astate = AbstractAddress.t - let ( <= ) ~lhs ~rhs = AbstractLocation.equal lhs rhs + let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs let join l1 l2 = - if AbstractLocation.equal l1 l2 then l1 else (* TODO: scary *) AbstractLocation.mk_fresh () + if AbstractAddress.equal l1 l2 then l1 else (* TODO: scary *) AbstractAddress.mk_fresh () let widen ~prev ~next ~num_iters:_ = join prev next - let pp = AbstractLocation.pp + let pp = AbstractAddress.pp end module Access = struct @@ -53,32 +53,64 @@ module Access = struct let pp = AccessPath.pp_access end -module MemoryEdges = AbstractDomain.InvertedMap (Access) (AbstractLocationDomain) +module MemoryEdges = AbstractDomain.InvertedMap (Access) (AbstractAddressDomain) module MemoryDomain = struct - include AbstractDomain.InvertedMap (AbstractLocation) (MemoryEdges) + include AbstractDomain.InvertedMap (AbstractAddress) (MemoryEdges) - let add_edge loc_src access loc_end memory = + let add_edge addr_src access addr_end memory = let edges = - match find_opt loc_src memory with Some edges -> edges | None -> MemoryEdges.empty + match find_opt addr_src memory with Some edges -> edges | None -> MemoryEdges.empty in - add loc_src (MemoryEdges.add access loc_end edges) memory + add addr_src (MemoryEdges.add access addr_end edges) memory - let find_edge_opt loc access memory = + let find_edge_opt addr access memory = let open Option.Monad_infix in - find_opt loc memory >>= MemoryEdges.find_opt access + find_opt addr memory >>= MemoryEdges.find_opt access end -module AliasingDomain = AbstractDomain.InvertedMap (Var) (AbstractLocationDomain) -module AbstractLocationsDomain = AbstractDomain.FiniteSet (AbstractLocation) -module InvalidLocationsDomain = AbstractLocationsDomain +module AliasingDomain = AbstractDomain.InvertedMap (Var) (AbstractAddressDomain) + +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 + + +module type InvalidAddressesDomain = sig + include AbstractDomain.S + + val empty : astate + + val add : AbstractAddress.t -> actor -> astate -> astate + + val get_invalidation : AbstractAddress.t -> astate -> actor option +end + +module InvalidAddressesDomain : InvalidAddressesDomain = struct + module InvalidationReason = struct + type astate = actor + + let join actor _ = actor + + let ( <= ) ~lhs:_ ~rhs:_ = true + + let widen ~prev ~next:_ ~num_iters:_ = prev + + let pp = pp_actor + end + + include AbstractDomain.Map (AbstractAddress) (InvalidationReason) + + let get_invalidation address invalids = find_opt address invalids +end type t = - {heap: MemoryDomain.astate; stack: AliasingDomain.astate; invalids: InvalidLocationsDomain.astate} + {heap: MemoryDomain.astate; stack: AliasingDomain.astate; invalids: InvalidAddressesDomain.astate} let initial = - {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty} + {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= InvalidAddressesDomain.empty} module Domain : AbstractDomain.S with type astate = t = struct @@ -91,7 +123,7 @@ module Domain : AbstractDomain.S with type astate = t = struct into the heap. *) let ( <= ) ~lhs ~rhs = phys_equal lhs rhs - || InvalidLocationsDomain.( <= ) ~lhs:lhs.invalids ~rhs:rhs.invalids + || InvalidAddressesDomain.( <= ) ~lhs:lhs.invalids ~rhs:rhs.invalids && AliasingDomain.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && MemoryDomain.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap @@ -102,7 +134,7 @@ module Domain : AbstractDomain.S with type astate = t = struct else { heap= MemoryDomain.join astate1.heap astate2.heap ; stack= AliasingDomain.join astate1.stack astate2.stack - ; invalids= InvalidLocationsDomain.join astate1.invalids astate2.invalids } + ; invalids= InvalidAddressesDomain.join astate1.invalids astate2.invalids } let max_widening = 5 @@ -116,117 +148,146 @@ module Domain : AbstractDomain.S with type astate = t = struct else { heap= MemoryDomain.widen ~num_iters ~prev:prev.heap ~next:next.heap ; stack= AliasingDomain.widen ~num_iters ~prev:prev.stack ~next:next.stack - ; invalids= InvalidLocationsDomain.widen ~num_iters ~prev:prev.invalids ~next:next.invalids + ; invalids= InvalidAddressesDomain.widen ~num_iters ~prev:prev.invalids ~next:next.invalids } let pp fmt {heap; stack; invalids} = F.fprintf fmt "{@[ heap=@[%a@];@;stack=@[%a@];@;invalids=@[%a@];@]}" - MemoryDomain.pp heap AliasingDomain.pp stack InvalidLocationsDomain.pp invalids + MemoryDomain.pp heap AliasingDomain.pp stack InvalidAddressesDomain.pp invalids end include Domain module Diagnostic = struct - (* TODO: more structured error type so that we can actually report something informative about - the variables being accessed along with a trace *) - type t = InvalidLocation of AbstractLocation.t + type t = + | AccessToInvalidAddress of + { invalidated_at: actor + ; accessed_by: actor + ; address: AbstractAddress.t } - let to_string (InvalidLocation loc) = F.asprintf "invalid location %a" AbstractLocation.pp loc -end + let get_location (AccessToInvalidAddress {accessed_by= {location}}) = location -type 'a access_result = ('a, t * Diagnostic.t) result + let get_message (AccessToInvalidAddress {accessed_by; invalidated_at; 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 + + + 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) + [] + ; Errlog.make_trace_element 0 accessed_by.location + (F.asprintf "accessed `%a` here" AccessExpression.pp accessed_by.access_expr) + [] ] -(** Check that the location is not known to be invalid *) -let check_loc_access loc astate = - if AbstractLocationsDomain.mem loc astate.invalids then - Error (astate, Diagnostic.InvalidLocation loc) - else Ok astate + let get_issue_type (AccessToInvalidAddress _) = IssueType.use_after_lifetime +end + +type 'a access_result = ('a, t * Diagnostic.t) result -(** Walk the heap starting from [loc] and following [path]. Stop either at the element before last - and return [new_loc] if [overwrite_last] is [Some new_loc], or go until the end of the path if it - is [None]. Create more locations into the heap as needed to follow the [path]. Check that each - location reached is valid. *) -let rec walk ~overwrite_last loc path astate = +(** 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 + (astate, Diagnostic.AccessToInvalidAddress {invalidated_at; accessed_by= actor; address}) + | None -> + Ok astate + + +(** Walk the heap starting from [addr] and following [path]. Stop either at the element before last + and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it + is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each + address reached is valid. *) +let rec walk actor ~overwrite_last addr path astate = match (path, overwrite_last) with | [], None -> - Ok (astate, loc) + Ok (astate, addr) | [], Some _ -> - L.die InternalError "Cannot overwrite last location in empty path" - | [a], Some new_loc -> - check_loc_access loc astate + L.die InternalError "Cannot overwrite last address in empty path" + | [a], Some new_addr -> + check_addr_access actor addr astate >>| fun astate -> - let heap = MemoryDomain.add_edge loc a new_loc astate.heap in - ({astate with heap}, new_loc) + let heap = MemoryDomain.add_edge addr a new_addr astate.heap in + ({astate with heap}, new_addr) | a :: path, _ -> ( - check_loc_access loc astate + check_addr_access actor addr astate >>= fun astate -> - match MemoryDomain.find_edge_opt loc a astate.heap with + match MemoryDomain.find_edge_opt addr a astate.heap with | None -> - let loc' = AbstractLocation.mk_fresh () in - let heap = MemoryDomain.add_edge loc a loc' astate.heap in + let addr' = AbstractAddress.mk_fresh () in + let heap = MemoryDomain.add_edge addr a addr' astate.heap in let astate = {astate with heap} in - walk ~overwrite_last loc' path astate - | Some loc' -> - walk ~overwrite_last loc' path astate ) + walk actor ~overwrite_last addr' path astate + | Some addr' -> + walk actor ~overwrite_last addr' path astate ) -(** add locations to the state to give a location to the destination of the given access path *) -let walk_access_expr ?overwrite_last astate access_expr = +(** 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 match (overwrite_last, access_list) with - | Some new_loc, [] -> - let stack = AliasingDomain.add access_var new_loc astate.stack in - Ok ({astate with stack}, new_loc) + | Some new_addr, [] -> + let stack = AliasingDomain.add access_var new_addr astate.stack in + Ok ({astate with stack}, new_addr) | None, _ | Some _, _ :: _ -> - let astate, base_loc = + let astate, base_addr = match AliasingDomain.find_opt access_var astate.stack with - | Some loc -> - (astate, loc) + | Some addr -> + (astate, addr) | None -> - let loc = AbstractLocation.mk_fresh () in - let stack = AliasingDomain.add access_var loc astate.stack in - ({astate with stack}, loc) + let addr = AbstractAddress.mk_fresh () in + let stack = AliasingDomain.add access_var addr astate.stack in + ({astate with stack}, addr) in - walk ~overwrite_last base_loc access_list astate + let actor = {access_expr; location} in + walk actor ~overwrite_last base_addr access_list astate (** Use the stack and heap to walk the access path represented by the given expression down to an - abstract location representing what the expression points to. + abstract address representing what the expression points to. - Return an error state if it traverses some known invalid location or if the end destination is + Return an error state if it traverses some known invalid address or if the end destination is known to be invalid. *) -let materialize_location astate access_expr = walk_access_expr astate access_expr +let materialize_address astate access_expr = walk_access_expr astate access_expr (** Use the stack and heap to walk the access path represented by the given expression down to an - abstract location representing what the expression points to, and replace that with the given - location. + abstract address representing what the expression points to, and replace that with the given + address. - Return an error state if it traverses some known invalid location. *) -let overwrite_location astate access_expr new_loc = - walk_access_expr ~overwrite_last:new_loc astate access_expr + Return an error state if it traverses some known invalid address. *) +let overwrite_address astate access_expr new_addr = + walk_access_expr ~overwrite_last:new_addr astate access_expr -(** Add the given location to the set of know invalid locations. *) -let mark_invalid loc astate = - {astate with invalids= AbstractLocationsDomain.add loc astate.invalids} +(** Add the given address to the set of know invalid addresses. *) +let mark_invalid actor address astate = + {astate with invalids= InvalidAddressesDomain.add address actor astate.invalids} -let read access_expr astate = - materialize_location astate access_expr - >>= fun (astate, loc) -> check_loc_access loc astate >>| fun astate -> (astate, loc) +let read 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 >>| fun astate -> (astate, addr) -let read_all access_exprs astate = +let read_all location access_exprs astate = List.fold_result access_exprs ~init:astate ~f:(fun astate access_expr -> - read access_expr astate >>| fst ) + read location access_expr astate >>| fst ) -let write access_expr loc astate = - overwrite_location astate access_expr loc >>| fun (astate, _) -> astate +let write location access_expr addr astate = + overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate -let invalidate access_expr astate = - materialize_location astate access_expr - >>= fun (astate, loc) -> check_loc_access loc astate >>| mark_invalid loc +let invalidate 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 diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index c897feb08..06036b57c 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -8,7 +8,7 @@ open! IStd module F = Format -module AbstractLocation : sig +module AbstractAddress : sig type t = private int [@@deriving compare] val mk_fresh : unit -> t @@ -22,27 +22,25 @@ module Access : sig val pp : F.formatter -> t -> unit end -module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLocation.t +module AbstractAddressDomain : AbstractDomain.S with type astate = AbstractAddress.t -module AbstractLocationsDomain : module type of AbstractDomain.FiniteSet (AbstractLocation) +module MemoryEdges : module type of AbstractDomain.InvertedMap (Access) (AbstractAddressDomain) -module MemoryEdges : module type of AbstractDomain.InvertedMap (Access) (AbstractLocationDomain) +module MemoryDomain : module type of AbstractDomain.InvertedMap (AbstractAddress) (MemoryEdges) -module MemoryDomain : module type of AbstractDomain.InvertedMap (AbstractLocation) (MemoryEdges) +module AliasingDomain : module type of AbstractDomain.InvertedMap (Var) (AbstractAddressDomain) -module AliasingDomain : module type of AbstractDomain.InvertedMap (Var) (AbstractLocationDomain) - -module InvalidLocationsDomain : module type of AbstractLocationsDomain +module InvalidAddressesDomain : AbstractDomain.S type t = { heap: MemoryDomain.astate - (** Symbolic representation of the heap: a graph where nodes are abstract locations and edges are + (** Symbolic representation of the heap: a graph where nodes are abstract addresses and edges are access path elements. *) ; stack: AliasingDomain.astate - (** Symbolic representation of the stack: which memory location do variables point to. No other + (** Symbolic representation of the stack: which memory address do variables point to. No other values are being tracked. *) - ; invalids: InvalidLocationsDomain.astate - (** Set of locations known to be in an invalid state. *) } + ; invalids: InvalidAddressesDomain.astate + (** Set of addresses known to be in an invalid state. *) } include AbstractDomain.S with type astate = t @@ -51,15 +49,21 @@ val initial : t module Diagnostic : sig type t - val to_string : t -> string + val get_message : t -> string + + val get_location : t -> Location.t + + val get_issue_type : t -> IssueType.t + + val get_trace : t -> Errlog.loc_trace end type 'a access_result = ('a, t * Diagnostic.t) result -val read : AccessExpression.t -> t -> (t * AbstractLocation.t) access_result +val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) access_result -val read_all : AccessExpression.t list -> t -> t access_result +val read_all : Location.t -> AccessExpression.t list -> t -> t access_result -val write : AccessExpression.t -> AbstractLocation.t -> t -> t access_result +val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result -val invalidate : AccessExpression.t -> t -> t access_result +val invalidate : Location.t -> AccessExpression.t -> t -> t access_result diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 6ef471bcf..47ff0ae4b 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -8,7 +8,8 @@ open! IStd open Result.Monad_infix type exec_fun = - ret:Var.t * Typ.t + Location.t + -> ret:Var.t * Typ.t -> actuals:HilExp.t list -> PulseDomain.t -> PulseDomain.t PulseDomain.access_result @@ -17,10 +18,10 @@ type model = exec_fun module Cplusplus = struct let delete : model = - fun ~ret:_ ~actuals astate -> + fun location ~ret:_ ~actuals astate -> match actuals with | [AccessExpression deleted_access] -> - PulseDomain.invalidate deleted_access astate + PulseDomain.invalidate location deleted_access astate | _ -> Ok astate end @@ -38,20 +39,20 @@ module StdVector = struct let at : model = - fun ~ret ~actuals astate -> + fun location ~ret ~actuals astate -> match actuals with | [AccessExpression vector; _index] -> - PulseDomain.read (deref_internal_array vector) astate - >>= fun (astate, loc) -> PulseDomain.write (AccessExpression.Base ret) loc astate + PulseDomain.read location (deref_internal_array vector) astate + >>= fun (astate, loc) -> PulseDomain.write location (AccessExpression.Base ret) loc astate | _ -> Ok astate let push_back : model = - fun ~ret:_ ~actuals astate -> + fun location ~ret:_ ~actuals astate -> match actuals with | [AccessExpression vector; _value] -> - PulseDomain.invalidate (deref_internal_array vector) astate + PulseDomain.invalidate location (deref_internal_array vector) astate | _ -> Ok astate end diff --git a/infer/src/checkers/PulseModels.mli b/infer/src/checkers/PulseModels.mli index b91074e27..dfd9aaee7 100644 --- a/infer/src/checkers/PulseModels.mli +++ b/infer/src/checkers/PulseModels.mli @@ -7,7 +7,8 @@ open! IStd type exec_fun = - ret:Var.t * Typ.t + Location.t + -> ret:Var.t * Typ.t -> actuals:HilExp.t list -> PulseDomain.t -> PulseDomain.t PulseDomain.access_result diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 7276aba99..9831a68f0 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,13 +1,13 @@ -codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_delete_throw_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, gated_exit_abort_ok, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [] -codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [] +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, 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/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated `&(x).__internal_array[_]` here,accessed `*(y)` here]