From 6d6ac1d3684242b5ef654374019dcd5e0b4f4ee2 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 26 Oct 2018 07:30:18 -0700 Subject: [PATCH] [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 | 85 +++++++++++----- infer/src/IR/AccessExpression.mli | 15 +++ infer/src/checkers/Pulse.ml | 15 ++- infer/src/checkers/PulseDomain.ml | 97 +++++++++++++++---- infer/src/checkers/PulseDomain.mli | 5 +- infer/src/checkers/PulseInvalidation.ml | 46 +++++---- infer/src/checkers/PulseInvalidation.mli | 16 +-- infer/src/checkers/PulseModels.ml | 11 ++- .../tests/codetoanalyze/cpp/pulse/issues.exp | 11 ++- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 10 +- 10 files changed, 228 insertions(+), 83 deletions(-) diff --git a/infer/src/IR/AccessExpression.ml b/infer/src/IR/AccessExpression.ml index 1516b8763..95fae2ddb 100644 --- a/infer/src/IR/AccessExpression.ml +++ b/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) diff --git a/infer/src/IR/AccessExpression.mli b/infer/src/IR/AccessExpression.mli index 0266d881c..873161b8a 100644 --- a/infer/src/IR/AccessExpression.mli +++ b/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 diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 5b7391894..93b0c04da 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 ) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index b2b9489fc..79106df08 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 - (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 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) + [] ) + |> 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 diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 65d7d4fa6..b54f75e7d 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/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 diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml index db9392d82..c08260f0c 100644 --- a/infer/src/checkers/PulseInvalidation.ml +++ b/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 diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli index 44f36aa21..9d1156b26 100644 --- a/infer/src/checkers/PulseInvalidation.mli +++ b/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 diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 825ef135d..4cfa63557 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 7e8dec71d..3fff821a9 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 12bd392c8..8cca254d9 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -7,9 +7,15 @@ #include #include -void deref_vector_element_after_lifetime_bad() { +void deref_vector_element_after_lifetime_bad(std::vector& x) { + int* y = &x[1]; + x.push_back(42); + std::cout << *y << "\n"; +} + +void deref_local_vector_element_after_lifetime_bad() { std::vector x = {0, 0}; int* y = &x[1]; - x.push_back(4); + x.push_back(42); std::cout << *y << "\n"; }