[pulse] no longer drop attributes of dead addresses

Summary:
When garbage-collecting addresses we would also remove their attributes.
But even though the addresses are no longer allocated in the heap, they
might show up in the formula and so we need to remember facts about
them.

This forces us to detect leaks closer to the point where addresses are
deleted from the heap, in AbductiveDomain.ml. This is a nice refactoring
in itself: doing so fixes some other FNs where we sometimes missed leak
detection on dead addresses.

This also makes it unecessary to simplify InstanceOf eagerly when
variables get out of scope.

Some new {folly,std}::optionals false positives that either are similar to existing ones or involve unmodelled smart pointers.

Reviewed By: da319

Differential Revision: D28126103

fbshipit-source-id: e3a903282
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent e5d52c3dc3
commit 16cb07698e

@ -206,7 +206,7 @@ module PulseTransferFunctions = struct
| Error _ as err -> | Error _ as err ->
Some err Some err
| Ok exec_state -> | Ok exec_state ->
PulseSummary.force_exit_program tenv proc_desc err_log exec_state PulseSummary.force_exit_program tenv proc_desc err_log call_loc exec_state
|> Option.map ~f:(fun exec_state -> Ok exec_state) ) |> Option.map ~f:(fun exec_state -> Ok exec_state) )
else exec_states_res else exec_states_res
@ -258,7 +258,7 @@ module PulseTransferFunctions = struct
[astate] [astate]
| ContinueProgram astate -> | ContinueProgram astate ->
dispatch_call analysis_data ret call_exp actuals location call_flags astate dispatch_call analysis_data ret call_exp actuals location call_flags astate
|> PulseReport.report_exec_results tenv proc_desc err_log ) |> PulseReport.report_exec_results tenv proc_desc err_log location )
in in
let dynamic_types_unreachable = let dynamic_types_unreachable =
PulseOperations.get_dynamic_type_unreachable_values vars astate PulseOperations.get_dynamic_type_unreachable_values vars astate
@ -296,7 +296,7 @@ module PulseTransferFunctions = struct
[ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
PulseOperations.write_id lhs_id rhs_addr_hist astate) ] PulseOperations.write_id lhs_id rhs_addr_hist astate) ]
in in
PulseReport.report_results tenv proc_desc err_log result PulseReport.report_results tenv proc_desc err_log loc result
in in
let set_global_astates = let set_global_astates =
match rhs_exp with match rhs_exp with
@ -369,7 +369,7 @@ module PulseTransferFunctions = struct
| _ -> | _ ->
astates astates
in in
PulseReport.report_results tenv proc_desc err_log result PulseReport.report_results tenv proc_desc err_log loc result
| Prune (condition, loc, _is_then_branch, _if_kind) -> | Prune (condition, loc, _is_then_branch, _if_kind) ->
(let<*> astate = PulseOperations.prune loc ~condition astate in (let<*> astate = PulseOperations.prune loc ~condition astate in
if PulseArithmetic.is_unsat_cheap astate then if PulseArithmetic.is_unsat_cheap astate then
@ -378,10 +378,10 @@ module PulseTransferFunctions = struct
else else
(* [condition] is true or unknown value: go into the branch *) (* [condition] is true or unknown value: go into the branch *)
[Ok (ContinueProgram astate)]) [Ok (ContinueProgram astate)])
|> PulseReport.report_exec_results tenv proc_desc err_log |> PulseReport.report_exec_results tenv proc_desc err_log loc
| Call (ret, call_exp, actuals, loc, call_flags) -> | Call (ret, call_exp, actuals, loc, call_flags) ->
dispatch_call analysis_data ret call_exp actuals loc call_flags astate dispatch_call analysis_data ret call_exp actuals loc call_flags astate
|> PulseReport.report_exec_results tenv proc_desc err_log |> PulseReport.report_exec_results tenv proc_desc err_log loc
| Metadata (ExitScope (vars, location)) -> | Metadata (ExitScope (vars, location)) ->
let remove_vars vars astates = let remove_vars vars astates =
List.concat_map astates ~f:(fun (astate : Domain.t) -> List.concat_map astates ~f:(fun (astate : Domain.t) ->
@ -393,8 +393,7 @@ module PulseTransferFunctions = struct
| LatentInvalidAccess _ -> | LatentInvalidAccess _ ->
[astate] [astate]
| ContinueProgram astate -> | ContinueProgram astate ->
PulseOperations.remove_vars tenv vars location astate [ContinueProgram (PulseOperations.remove_vars vars location astate)] )
|> PulseReport.report_result tenv proc_desc err_log )
in in
if Procname.is_java (Procdesc.get_proc_name proc_desc) then if Procname.is_java (Procdesc.get_proc_name proc_desc) then
remove_vars vars [ContinueProgram astate] remove_vars vars [ContinueProgram astate]
@ -461,7 +460,11 @@ let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data
let updated_posts = let updated_posts =
PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts
in in
let summary = PulseSummary.of_posts tenv proc_desc err_log updated_posts in let summary =
PulseSummary.of_posts tenv proc_desc err_log
(Procdesc.get_exit_node proc_desc |> Procdesc.Node.get_loc)
updated_posts
in
report_topl_errors proc_desc err_log summary ; report_topl_errors proc_desc err_log summary ;
Some summary ) Some summary )
| None -> | None ->

@ -35,7 +35,7 @@ module type BaseDomainSig_ = sig
(** filter both heap and attrs *) (** filter both heap and attrs *)
val filter_addr_with_discarded_addrs : val filter_addr_with_discarded_addrs :
f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list heap_only:bool -> f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list
(** compute new state containing only reachable addresses in its heap and attributes, as well as (** compute new state containing only reachable addresses in its heap and attributes, as well as
the list of discarded unreachable addresses *) the list of discarded unreachable addresses *)
@ -76,10 +76,11 @@ end = struct
update ~heap:heap' ~attrs:attrs' foot update ~heap:heap' ~attrs:attrs' foot
let filter_addr_with_discarded_addrs ~f foot = let filter_addr_with_discarded_addrs ~heap_only ~f foot =
let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in
let attrs', discarded_addresses = let attrs', discarded_addresses =
BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs if heap_only then (foot.attrs, [])
else BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs
in in
(update ~heap:heap' ~attrs:attrs' foot, discarded_addresses) (update ~heap:heap' ~attrs:attrs' foot, discarded_addresses)
@ -130,16 +131,6 @@ let leq ~lhs ~rhs =
let initialize address astate = {astate with post= PostDomain.initialize address astate.post} let initialize address astate = {astate with post= PostDomain.initialize address astate.post}
let simplify_instanceof tenv astate =
let attrs = (astate.post :> BaseDomain.t).attrs in
let path_condition =
PathCondition.simplify_instanceof tenv
~get_dynamic_type:(BaseAddressAttributes.get_dynamic_type attrs)
astate.path_condition
in
{astate with path_condition}
module Stack = struct module Stack = struct
let is_abducible astate var = let is_abducible astate var =
(* HACK: formals are pre-registered in the initial state *) (* HACK: formals are pre-registered in the initial state *)
@ -613,14 +604,42 @@ let skipped_calls_match_pattern astate =
astate.skipped_calls ) astate.skipped_calls )
let discard_unreachable ({pre; post} as astate) = let check_memory_leaks unreachable_addrs astate =
let check_memory_leak attributes =
let allocated_not_freed_opt =
Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *))
~f:(fun acc attr ->
match (attr : Attribute.t) with
| Allocated (procname, trace) ->
(Some (procname, trace), snd acc)
| Invalid (CFree, _) ->
(fst acc, true)
| _ ->
acc )
in
match allocated_not_freed_opt with
| Some (procname, trace), false ->
(* allocated but not freed *)
Error (procname, trace)
| _ ->
Ok ()
in
List.fold_result unreachable_addrs ~init:() ~f:(fun () addr ->
match AddressAttributes.find_opt addr astate with
| Some unreachable_attrs ->
check_memory_leak unreachable_attrs
| None ->
Ok () )
let discard_unreachable_ ~for_summary ({pre; post} as astate) =
let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in
let pre_new = let pre_new =
PreDomain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address pre_addresses) pre PreDomain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address pre_addresses) pre
in in
let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
let post_new, discard_addresses = let post_new, dead_addresses =
PostDomain.filter_addr_with_discarded_addrs PostDomain.filter_addr_with_discarded_addrs ~heap_only:(not for_summary)
~f:(fun address -> ~f:(fun address ->
AbstractValue.Set.mem address pre_addresses || AbstractValue.Set.mem address post_addresses AbstractValue.Set.mem address pre_addresses || AbstractValue.Set.mem address post_addresses
) )
@ -631,7 +650,25 @@ let discard_unreachable ({pre; post} as astate) =
if phys_equal pre_new pre && phys_equal post_new post then astate if phys_equal pre_new pre && phys_equal post_new post then astate
else {astate with pre= pre_new; post= post_new} else {astate with pre= pre_new; post= post_new}
in in
(astate, pre_addresses, post_addresses, discard_addresses) (astate, pre_addresses, post_addresses, dead_addresses)
(* exported in .mli *)
let discard_unreachable astate =
let astate, _pre_addresses, _post_addresses, _dead_addresses =
discard_unreachable_ ~for_summary:false astate
in
(* NOTE: [_dead_addresses] is always the empty list when [for_summary] is [false] *)
astate
let get_unreachable_attributes {post} =
let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
BaseAddressAttributes.fold
(fun address _ dead_addresses ->
if AbstractValue.Set.mem address post_addresses then dead_addresses
else address :: dead_addresses )
(post :> BaseDomain.t).attrs []
let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
@ -875,7 +912,9 @@ let filter_for_summary tenv proc_name astate0 =
this. *) this. *)
let astate = restore_formals_for_summary astate_before_filter in let astate = restore_formals_for_summary astate_before_filter in
let astate = {astate with topl= PulseTopl.filter_for_summary astate.path_condition astate.topl} in let astate = {astate with topl= PulseTopl.filter_for_summary astate.path_condition astate.topl} in
let astate, pre_live_addresses, post_live_addresses, _ = discard_unreachable astate in let astate, pre_live_addresses, post_live_addresses, dead_addresses =
discard_unreachable_ ~for_summary:true astate
in
let can_be_pruned = let can_be_pruned =
if PatternMatch.is_entry_point proc_name then if PatternMatch.is_entry_point proc_name then
(* report all latent issues at entry points *) (* report all latent issues at entry points *)
@ -889,10 +928,12 @@ let filter_for_summary tenv proc_name astate0 =
(BaseAddressAttributes.get_dynamic_type (astate_before_filter.post :> BaseDomain.t).attrs) (BaseAddressAttributes.get_dynamic_type (astate_before_filter.post :> BaseDomain.t).attrs)
~can_be_pruned ~keep:live_addresses astate.path_condition ~can_be_pruned ~keep:live_addresses astate.path_condition
in in
({astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}, new_eqs) ( {astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}
, dead_addresses
, new_eqs )
let summary_of_post tenv pdesc astate = let summary_of_post tenv pdesc location astate =
let open SatUnsat.Import in let open SatUnsat.Import in
(* NOTE: we normalize (to strengthen the equality relation used by canonicalization) then (* NOTE: we normalize (to strengthen the equality relation used by canonicalization) then
canonicalize *before* garbage collecting unused addresses in case we detect any last-minute canonicalize *before* garbage collecting unused addresses in case we detect any last-minute
@ -905,13 +946,20 @@ let summary_of_post tenv pdesc astate =
let* () = if is_unsat then Unsat else Sat () in let* () = if is_unsat then Unsat else Sat () in
let astate = {astate with path_condition} in let astate = {astate with path_condition} in
let* astate, error = incorporate_new_eqs astate new_eqs in let* astate, error = incorporate_new_eqs astate new_eqs in
let* astate, new_eqs = filter_for_summary tenv (Procdesc.get_proc_name pdesc) astate in let astate_before_filter = astate in
let* astate, dead_addresses, new_eqs =
filter_for_summary tenv (Procdesc.get_proc_name pdesc) astate
in
let+ astate, error = let+ astate, error =
match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error) match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error)
in in
match error with match error with
| None -> | None -> (
Ok (invalidate_locals pdesc astate) match check_memory_leaks dead_addresses astate_before_filter with
| Ok () ->
Ok (invalidate_locals pdesc astate)
| Error (proc_name, trace) ->
Error (`MemoryLeak (astate, proc_name, trace, location)) )
| Some (address, must_be_valid) -> | Some (address, must_be_valid) ->
Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid)) Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))

@ -57,8 +57,6 @@ val get_pre : t -> BaseDomain.t
val get_post : t -> BaseDomain.t val get_post : t -> BaseDomain.t
val simplify_instanceof : Tenv.t -> t -> t
(** stack operations like {!BaseStack} but that also take care of propagating facts to the (** stack operations like {!BaseStack} but that also take care of propagating facts to the
precondition *) precondition *)
module Stack : sig module Stack : sig
@ -158,10 +156,11 @@ val is_local : Var.t -> t -> bool
val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option
val discard_unreachable : t -> t * AbstractValue.Set.t * AbstractValue.Set.t * AbstractValue.t list val discard_unreachable : t -> t
(** garbage collect unreachable addresses in the state to make it smaller and return the new state, (** garbage collect unreachable addresses in the state to make it smaller and return the new state *)
the live pre addresses, the live post addresses, and the discarded addresses that used to have
attributes attached *) val get_unreachable_attributes : t -> AbstractValue.t list
(** collect the addresses that have attributes but are unreachable in the current post-condition *)
val add_skipped_call : Procname.t -> Trace.t -> t -> t val add_skipped_call : Procname.t -> Trace.t -> t -> t
@ -181,14 +180,16 @@ val skipped_calls_match_pattern : summary -> bool
val summary_of_post : val summary_of_post :
Tenv.t Tenv.t
-> Procdesc.t -> Procdesc.t
-> Location.t
-> t -> t
-> ( summary -> ( summary
, [> `PotentialInvalidAccessSummary of , [> `MemoryLeak of summary * Procname.t * Trace.t * Location.t
summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] ) | `PotentialInvalidAccessSummary of
summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) ] )
result result
SatUnsat.t SatUnsat.t
(** trim the state down to just the procedure's interface (formals and globals), and simplify and (** Trim the state down to just the procedure's interface (formals and globals), and simplify and
normalize the state *) normalize the state. *)
val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t
(** directly set the edges for the given address, bypassing abduction altogether *) (** directly set the edges for the given address, bypassing abduction altogether *)

@ -19,6 +19,7 @@ type 'astate error =
; address: AbstractValue.t ; address: AbstractValue.t
; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t}
| ISLError of 'astate | ISLError of 'astate
type ('a, 'astate) base_t = ('a, 'astate error) result type ('a, 'astate) base_t = ('a, 'astate error) result
@ -33,6 +34,13 @@ type 'astate abductive_error =
AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option)
] ]
let ignore_memory_leaks = function
| Ok astate | Error (`MemoryLeak (astate, _, _, _)) ->
Ok astate
| Error #abductive_error as result ->
result
let of_abductive_error = function let of_abductive_error = function
| `ISLError astate -> | `ISLError astate ->
ISLError astate ISLError astate

@ -19,6 +19,7 @@ type 'astate error =
; address: AbstractValue.t ; address: AbstractValue.t
; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t}
| ISLError of 'astate | ISLError of 'astate
type ('a, 'astate) base_t = ('a, 'astate error) result type ('a, 'astate) base_t = ('a, 'astate error) result
@ -26,7 +27,10 @@ type ('a, 'astate) base_t = ('a, 'astate error) result
type 'a t = ('a, AbductiveDomain.t) base_t type 'a t = ('a, AbductiveDomain.t) base_t
(** Intermediate datatype since {!AbductiveDomain} cannot refer to this module without creating a (** Intermediate datatype since {!AbductiveDomain} cannot refer to this module without creating a
circular dependency. *) circular dependency.
Purposefully omits [`MemoryLeak] errors as it's a good idea to double-check if you really want
to report a leak. *)
type 'astate abductive_error = type 'astate abductive_error =
[ `ISLError of 'astate [ `ISLError of 'astate
| `PotentialInvalidAccess of | `PotentialInvalidAccess of
@ -35,11 +39,18 @@ type 'astate abductive_error =
AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option) AbductiveDomain.summary * AbstractValue.t * (Trace.t * Invalidation.must_be_valid_reason option)
] ]
val of_abductive_error : 'astate abductive_error -> 'astate error val of_abductive_error : [< 'astate abductive_error] -> 'astate error
val of_abductive_result : ('a, 'astate abductive_error) result -> ('a, 'astate) base_t val of_abductive_result : ('a, [< 'astate abductive_error]) result -> ('a, 'astate) base_t
val of_abductive_access_result : val of_abductive_access_result :
Trace.t Trace.t
-> ('a, [`InvalidAccess of Invalidation.t * Trace.t * 'astate | 'astate abductive_error]) result -> ('a, [< `InvalidAccess of Invalidation.t * Trace.t * 'astate | 'astate abductive_error]) result
-> ('a, 'astate) base_t -> ('a, 'astate) base_t
val ignore_memory_leaks :
( AbductiveDomain.summary
, [< `MemoryLeak of AbductiveDomain.summary * Procname.t * Trace.t * Location.t
| AbductiveDomain.summary abductive_error ] )
result
-> (AbductiveDomain.summary, [> AbductiveDomain.summary abductive_error]) result

@ -117,8 +117,10 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
(astate :> AbductiveDomain.t) (astate :> AbductiveDomain.t)
~f:(fun subst astate -> ~f:(fun subst astate ->
let* astate_summary_result = let* astate_summary_result =
AbductiveDomain.summary_of_post tenv caller_proc_desc astate ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate
>>| AccessResult.of_abductive_result >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result
:> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t
)
in in
match astate_summary_result with match astate_summary_result with
| Error _ as error -> | Error _ as error ->
@ -140,11 +142,9 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
| `DelayReport latent_issue -> | `DelayReport latent_issue ->
Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue}))
| `ReportNow -> | `ReportNow ->
Sat Sat (Error (ReportableErrorSummary {diagnostic; astate= astate_summary}))
(Error
(ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)}))
| `ISLDelay astate -> | `ISLDelay astate ->
Sat (Error (ISLError (astate :> AbductiveDomain.t))) ) Sat (Error (ISLError astate)) )
| LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> ( | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> (
match AbstractValue.Map.find_opt address_callee subst with match AbstractValue.Map.find_opt address_callee subst with
| None -> | None ->
@ -167,7 +167,7 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
| Some (invalidation, invalidation_trace) -> | Some (invalidation, invalidation_trace) ->
Sat Sat
(Error (Error
(ReportableError (ReportableErrorSummary
{ diagnostic= { diagnostic=
AccessToInvalidAddress AccessToInvalidAddress
{ calling_context { calling_context
@ -175,13 +175,14 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
; invalidation_trace ; invalidation_trace
; access_trace= fst must_be_valid ; access_trace= fst must_be_valid
; must_be_valid_reason= snd must_be_valid } ; must_be_valid_reason= snd must_be_valid }
; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) ) ; astate= astate_summary })) ) ) ) )
| ISLLatentMemoryError astate -> | ISLLatentMemoryError astate ->
map_call_result ~is_isl_error_prepost:true map_call_result ~is_isl_error_prepost:true
(astate :> AbductiveDomain.t) (astate :> AbductiveDomain.t)
~f:(fun _subst astate -> ~f:(fun _subst astate ->
AbductiveDomain.summary_of_post tenv caller_proc_desc astate ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate
>>| AccessResult.of_abductive_result >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result
:> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t )
>>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) ) >>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) )

@ -77,10 +77,3 @@ val has_no_assumptions : t -> bool
val get_var_repr : t -> Var.t -> Var.t val get_var_repr : t -> Var.t -> Var.t
(** get the canonical representative for the variable according to the equality relation *) (** get the canonical representative for the variable according to the equality relation *)
(** Module for reasoning about dynamic types. **)
module DynamicTypes : sig
val simplify : Tenv.t -> get_dynamic_type:(Var.t -> Typ.t option) -> t -> t
(** Simplifies [IsInstanceOf(var, typ)] predicate when dynamic type information is available in
state. **)
end

@ -49,10 +49,12 @@ module Misc = struct
let early_exit : model = let early_exit : model =
fun {analysis_data= {tenv; proc_desc}} astate -> fun {analysis_data= {tenv; proc_desc}; location} astate ->
let open SatUnsat.Import in let open SatUnsat.Import in
match match
AbductiveDomain.summary_of_post tenv proc_desc astate >>| AccessResult.of_abductive_result ( AbductiveDomain.summary_of_post tenv proc_desc location astate
>>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result
:> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t )
with with
| Unsat -> | Unsat ->
[] []

@ -85,7 +85,7 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in
PulseArithmetic.prune_positive (fst value) astate PulseArithmetic.prune_positive (fst value) astate
in in
PulseReport.report_result tenv proc_desc err_log result PulseReport.report_result tenv proc_desc err_log location result
| ExitProgram _ | ExitProgram _
| AbortProgram _ | AbortProgram _
| LatentAbortProgram _ | LatentAbortProgram _
@ -120,7 +120,7 @@ let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_lo
in in
astate astate
in in
PulseReport.report_result tenv proc_desc err_log result PulseReport.report_result tenv proc_desc err_log location result
| ContinueProgram _, _ | ContinueProgram _, _
| ExitProgram _, _ | ExitProgram _, _
| AbortProgram _, _ | AbortProgram _, _
@ -136,6 +136,7 @@ let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log}
| None -> | None ->
List.concat_map ~f:(update_must_be_valid_reason analysis_data) posts List.concat_map ~f:(update_must_be_valid_reason analysis_data) posts
| Some result -> | Some result ->
let nil_summary = PulseReport.report_result tenv proc_desc err_log result in let location = Procdesc.get_loc proc_desc in
let nil_summary = PulseReport.report_result tenv proc_desc err_log location result in
let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in
nil_summary @ posts nil_summary @ posts

@ -37,6 +37,7 @@ module Import = struct
; address: AbstractValue.t ; address: AbstractValue.t
; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t}
| ISLError of 'astate | ISLError of 'astate
include IResult.Let_syntax include IResult.Let_syntax
@ -512,37 +513,6 @@ let mark_address_of_stack_variable history variable location address astate =
AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate
let check_memory_leak_unreachable unreachable_addrs location astate =
let check_memory_leak result attributes =
let allocated_not_freed_opt =
Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *))
~f:(fun acc attr ->
match (attr : Attribute.t) with
| Allocated (procname, trace) ->
(Some (procname, trace), snd acc)
| Invalid (CFree, _) ->
(fst acc, true)
| _ ->
acc )
in
match allocated_not_freed_opt with
| Some (procname, trace), false ->
(* allocated but not freed *)
Error
(ReportableError
{ diagnostic= Diagnostic.MemoryLeak {procname; location; allocation_trace= trace}
; astate })
| _ ->
result
in
List.fold unreachable_addrs ~init:(Ok ()) ~f:(fun res addr ->
match AbductiveDomain.AddressAttributes.find_opt addr astate with
| Some unreachable_attrs ->
check_memory_leak res unreachable_attrs
| None ->
res )
let get_dynamic_type_unreachable_values vars astate = let get_dynamic_type_unreachable_values vars astate =
(* For each unreachable address we find a root variable for it; if there is (* For each unreachable address we find a root variable for it; if there is
more than one, it doesn't matter which *) more than one, it doesn't matter which *)
@ -553,7 +523,7 @@ let get_dynamic_type_unreachable_values vars astate =
astate None astate None
in in
let astate' = Stack.remove_vars vars astate in let astate' = Stack.remove_vars vars astate in
let _, _, _, unreachable_addrs = AbductiveDomain.discard_unreachable astate' in let unreachable_addrs = AbductiveDomain.get_unreachable_attributes astate' in
let res = let res =
List.fold unreachable_addrs ~init:[] ~f:(fun res addr -> List.fold unreachable_addrs ~init:[] ~f:(fun res addr ->
(let open IOption.Let_syntax in (let open IOption.Let_syntax in
@ -566,13 +536,9 @@ let get_dynamic_type_unreachable_values vars astate =
List.map ~f:(fun (var, _, typ) -> (var, typ)) res List.map ~f:(fun (var, _, typ) -> (var, typ)) res
let remove_vars tenv vars location orig_astate = let remove_vars vars location orig_astate =
let astate = let astate =
(* Simplification of [IsInstanceOf(var, typ)] term is necessary here, as a variable can die before List.fold vars ~init:orig_astate ~f:(fun astate var ->
the normalization function is called. This could cause [IsInstanceOf(var, typ)] terms that
reference dead vars to be collected before they are evaluated to detect a contradiction *)
List.fold vars ~init:(AbductiveDomain.simplify_instanceof tenv orig_astate)
~f:(fun astate var ->
match Stack.find_opt var astate with match Stack.find_opt var astate with
| Some (address, history) -> | Some (address, history) ->
let astate = let astate =
@ -587,11 +553,7 @@ let remove_vars tenv vars location orig_astate =
astate ) astate )
in in
let astate' = Stack.remove_vars vars astate in let astate' = Stack.remove_vars vars astate in
if phys_equal astate' astate then Ok astate if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate'
else
let astate, _, _, unreachable_addrs = AbductiveDomain.discard_unreachable astate' in
let+ () = check_memory_leak_unreachable unreachable_addrs location orig_astate in
astate
let get_captured_actuals location ~captured_vars ~actual_closure astate = let get_captured_actuals location ~captured_vars ~actual_closure astate =

@ -44,6 +44,7 @@ module Import : sig
; address: AbstractValue.t ; address: AbstractValue.t
; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option } ; must_be_valid: Trace.t * Invalidation.must_be_valid_reason option }
| ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
| ReportableErrorSummary of {astate: AbductiveDomain.summary; diagnostic: Diagnostic.t}
| ISLError of 'astate | ISLError of 'astate
(** {2 Monadic syntax} *) (** {2 Monadic syntax} *)
@ -219,7 +220,7 @@ val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.t) lis
(** Given a list of variables, computes the unreachable values if the variables were removed from (** Given a list of variables, computes the unreachable values if the variables were removed from
the stack, then return the dynamic types of those values if they are available *) the stack, then return the dynamic types of those values if they are available *)
val remove_vars : Tenv.t -> Var.t list -> Location.t -> t -> t AccessResult.t val remove_vars : Var.t list -> Location.t -> t -> t
val check_address_escape : val check_address_escape :
Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t

@ -121,11 +121,6 @@ let simplify tenv ~can_be_pruned ~keep ~get_dynamic_type phi =
if (fst result).is_unsat then Unsat else Sat result if (fst result).is_unsat then Unsat else Sat result
let simplify_instanceof tenv ~get_dynamic_type phi =
let formula = Formula.DynamicTypes.simplify tenv ~get_dynamic_type phi.formula in
{phi with formula}
let subst_find_or_new subst addr_callee = let subst_find_or_new subst addr_callee =
match AbstractValue.Map.find_opt addr_callee subst with match AbstractValue.Map.find_opt addr_callee subst with
| None -> | None ->

@ -45,8 +45,6 @@ val simplify :
in [keep] as possible, and tries to eliminate variables not in [can_be_pruned] from the "pruned" in [keep] as possible, and tries to eliminate variables not in [can_be_pruned] from the "pruned"
part of the formula *) part of the formula *)
val simplify_instanceof : Tenv.t -> get_dynamic_type:(AbstractValue.t -> Typ.t option) -> t -> t
val and_callee : val and_callee :
(AbstractValue.t * ValueHistory.t) AbstractValue.Map.t (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t
-> t -> t

@ -47,33 +47,37 @@ let is_suppressed tenv proc_desc diagnostic astate =
false false
let summary_of_error_post tenv proc_desc mk_error astate = let summary_of_error_post tenv proc_desc location mk_error astate =
match AbductiveDomain.summary_of_post tenv proc_desc astate with match AbductiveDomain.summary_of_post tenv proc_desc location astate with
| Sat (Ok astate) -> | Sat (Ok astate) | Sat (Error (`MemoryLeak (astate, _, _, _))) ->
(* ignore potential memory leaks: error'ing in the middle of a function will typically produce
spurious leaks *)
Sat (mk_error astate) Sat (mk_error astate)
| Sat (Error error) -> | Sat (Error (`PotentialInvalidAccessSummary (summary, addr, trace))) ->
(* ignore the error we wanted to report (with [mk_error]): the abstract state contained a (* ignore the error we wanted to report (with [mk_error]): the abstract state contained a
potential error already so report [error] instead *) potential error already so report [error] instead *)
Sat (AccessResult.of_abductive_error error) Sat (AccessResult.of_abductive_error (`PotentialInvalidAccessSummary (summary, addr, trace)))
| Unsat -> | Unsat ->
Unsat Unsat
let summary_error_of_error tenv proc_desc (error : AbductiveDomain.t AccessResult.error) : let summary_error_of_error tenv proc_desc location (error : AbductiveDomain.t AccessResult.error) :
AbductiveDomain.summary AccessResult.error SatUnsat.t = AbductiveDomain.summary AccessResult.error SatUnsat.t =
match error with match error with
| PotentialInvalidAccessSummary {astate; address; must_be_valid} -> | PotentialInvalidAccessSummary {astate; address; must_be_valid} ->
Sat (PotentialInvalidAccessSummary {astate; address; must_be_valid}) Sat (PotentialInvalidAccessSummary {astate; address; must_be_valid})
| PotentialInvalidAccess {astate; address; must_be_valid} -> | PotentialInvalidAccess {astate; address; must_be_valid} ->
summary_of_error_post tenv proc_desc summary_of_error_post tenv proc_desc location
(fun astate -> PotentialInvalidAccess {astate; address; must_be_valid}) (fun astate -> PotentialInvalidAccess {astate; address; must_be_valid})
astate astate
| ReportableError {astate; diagnostic} -> | ReportableError {astate; diagnostic} ->
summary_of_error_post tenv proc_desc summary_of_error_post tenv proc_desc location
(fun astate -> ReportableError {astate; diagnostic}) (fun astate -> ReportableError {astate; diagnostic})
astate astate
| ReportableErrorSummary {astate; diagnostic} ->
Sat (ReportableErrorSummary {astate; diagnostic})
| ISLError astate -> | ISLError astate ->
summary_of_error_post tenv proc_desc (fun astate -> ISLError astate) astate summary_of_error_post tenv proc_desc location (fun astate -> ISLError astate) astate
let report_summary_error tenv proc_desc err_log let report_summary_error tenv proc_desc err_log
@ -92,7 +96,7 @@ let report_summary_error tenv proc_desc err_log
LatentInvalidAccess {astate; address; must_be_valid; calling_context= []} LatentInvalidAccess {astate; address; must_be_valid; calling_context= []}
| ISLError astate -> | ISLError astate ->
ISLLatentMemoryError astate ISLLatentMemoryError astate
| ReportableError {astate; diagnostic} -> ( | ReportableError {astate; diagnostic} | ReportableErrorSummary {astate; diagnostic} -> (
match LatentIssue.should_report astate diagnostic with match LatentIssue.should_report astate diagnostic with
| `ReportNow -> | `ReportNow ->
if not (is_suppressed tenv proc_desc diagnostic astate) then if not (is_suppressed tenv proc_desc diagnostic astate) then
@ -103,30 +107,33 @@ let report_summary_error tenv proc_desc err_log
LatentAbortProgram {astate; latent_issue} ) LatentAbortProgram {astate; latent_issue} )
let report_error tenv proc_desc err_log (access_error : AbductiveDomain.t AccessResult.error) = let report_error tenv proc_desc err_log location
(access_error : AbductiveDomain.t AccessResult.error) =
let open SatUnsat.Import in let open SatUnsat.Import in
summary_error_of_error tenv proc_desc access_error >>| report_summary_error tenv proc_desc err_log summary_error_of_error tenv proc_desc location access_error
>>| report_summary_error tenv proc_desc err_log
let report_exec_results tenv proc_desc err_log results = let report_exec_results tenv proc_desc err_log location results =
List.filter_map results ~f:(fun exec_result -> List.filter_map results ~f:(fun exec_result ->
match exec_result with match exec_result with
| Ok post -> | Ok post ->
Some post Some post
| Error error -> ( | Error error -> (
match report_error tenv proc_desc err_log error with match report_error tenv proc_desc err_log location error with
| Unsat -> | Unsat ->
None None
| Sat exec_state -> | Sat exec_state ->
Some exec_state ) ) Some exec_state ) )
let report_results tenv proc_desc err_log results = let report_results tenv proc_desc err_log location results =
let open IResult.Let_syntax in let open IResult.Let_syntax in
List.map results ~f:(fun result -> List.map results ~f:(fun result ->
let+ astate = result in let+ astate = result in
ExecutionDomain.ContinueProgram astate ) ExecutionDomain.ContinueProgram astate )
|> report_exec_results tenv proc_desc err_log |> report_exec_results tenv proc_desc err_log location
let report_result tenv proc_desc err_log result = report_results tenv proc_desc err_log [result] let report_result tenv proc_desc err_log location result =
report_results tenv proc_desc err_log location [result]

@ -9,7 +9,12 @@ open! IStd
open PulseDomainInterface open PulseDomainInterface
val report_result : val report_result :
Tenv.t -> Procdesc.t -> Errlog.t -> AbductiveDomain.t AccessResult.t -> ExecutionDomain.t list Tenv.t
-> Procdesc.t
-> Errlog.t
-> Location.t
-> AbductiveDomain.t AccessResult.t
-> ExecutionDomain.t list
val report_summary_error : val report_summary_error :
Tenv.t Tenv.t
@ -22,6 +27,7 @@ val report_results :
Tenv.t Tenv.t
-> Procdesc.t -> Procdesc.t
-> Errlog.t -> Errlog.t
-> Location.t
-> AbductiveDomain.t AccessResult.t list -> AbductiveDomain.t AccessResult.t list
-> ExecutionDomain.t list -> ExecutionDomain.t list
@ -29,5 +35,6 @@ val report_exec_results :
Tenv.t Tenv.t
-> Procdesc.t -> Procdesc.t
-> Errlog.t -> Errlog.t
-> Location.t
-> ExecutionDomain.t AccessResult.t list -> ExecutionDomain.t AccessResult.t list
-> ExecutionDomain.t list -> ExecutionDomain.t list

@ -21,15 +21,19 @@ let pp fmt summary =
F.close_box () F.close_box ()
let exec_summary_of_post_common tenv ~continue_program proc_desc err_log let exec_summary_of_post_common tenv ~continue_program proc_desc err_log location
(exec_astate : ExecutionDomain.t) : _ ExecutionDomain.base_t option = (exec_astate : ExecutionDomain.t) : _ ExecutionDomain.base_t option =
match exec_astate with match exec_astate with
| ContinueProgram astate -> ( | ContinueProgram astate -> (
match AbductiveDomain.summary_of_post tenv proc_desc astate with match AbductiveDomain.summary_of_post tenv proc_desc location astate with
| Unsat -> | Unsat ->
None None
| Sat (Ok astate) -> | Sat (Ok astate) ->
Some (continue_program astate) Some (continue_program astate)
| Sat (Error (`MemoryLeak (astate, procname, allocation_trace, location))) ->
Some
(PulseReport.report_summary_error tenv proc_desc err_log
(ReportableError {astate; diagnostic= MemoryLeak {procname; allocation_trace; location}}))
| Sat (Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))) -> ( | Sat (Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))) -> (
match match
AbductiveDomain.find_post_cell_opt address (astate :> AbductiveDomain.t) AbductiveDomain.find_post_cell_opt address (astate :> AbductiveDomain.t)
@ -67,8 +71,8 @@ let force_exit_program tenv proc_desc err_log post =
ExitProgram astate ) ExitProgram astate )
let of_posts tenv proc_desc err_log posts = let of_posts tenv proc_desc err_log location posts =
List.filter_mapi posts ~f:(fun i exec_state -> List.filter_mapi posts ~f:(fun i exec_state ->
L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ; L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ;
exec_summary_of_post_common tenv proc_desc err_log exec_state ~continue_program:(fun astate -> exec_summary_of_post_common tenv proc_desc err_log location exec_state
ContinueProgram astate ) ) ~continue_program:(fun astate -> ContinueProgram astate) )

@ -10,9 +10,14 @@ open PulseDomainInterface
type t = ExecutionDomain.summary list [@@deriving yojson_of] type t = ExecutionDomain.summary list [@@deriving yojson_of]
val of_posts : Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t list -> t val of_posts : Tenv.t -> Procdesc.t -> Errlog.t -> Location.t -> ExecutionDomain.t list -> t
val force_exit_program : val force_exit_program :
Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option Tenv.t
-> Procdesc.t
-> Errlog.t
-> Location.t
-> ExecutionDomain.t
-> _ ExecutionDomain.base_t option
val pp : Format.formatter -> t -> unit val pp : Format.formatter -> t -> unit

@ -9,14 +9,18 @@ codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, NULLPTR_DEREFERENCE, n
codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] codetoanalyze/c/pulse/latent.c, latent_use_after_free, 4, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here]
codetoanalyze/c/pulse/latent.c, main, 3, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] codetoanalyze/c/pulse/latent.c, main, 3, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here]
codetoanalyze/c/pulse/latent.c, manifest_use_after_free, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here] codetoanalyze/c/pulse/latent.c, manifest_use_after_free, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `latent_use_after_free`,invalidation part of the trace starts here,parameter `x` of latent_use_after_free,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of latent_use_after_free,invalid access occurs here]
codetoanalyze/c/pulse/memory_leak.c, malloc_formal_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 5, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, create_null_path2_latent, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of create_null_path2_latent,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here]

@ -34,3 +34,5 @@ void malloc_interproc_no_free_bad2() {
int y = 4; int y = 4;
int* q = p; int* q = p;
} }
void malloc_formal_leak_bad(int* x) { x = (int*)malloc(sizeof(int*)); }

@ -25,7 +25,7 @@ void call_create_null_path_then_deref_unconditionally_ok(int* p) {
*p = 52; *p = 52;
} }
void create_null_path2_ok(int* p) { void create_null_path2_latent(int* p) {
int* q = NULL; int* q = NULL;
if (p) { if (p) {
*p = 32; *p = 32;
@ -115,3 +115,9 @@ void bug_with_allocation_bad(int* x) {
int* y = NULL; int* y = NULL;
*y = 42; *y = 42;
} }
void null_alias_bad(int* x) {
int* y = NULL;
x = (int*)malloc(sizeof(int*));
*x = 42;
}

@ -54,6 +54,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, US
codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of set_x_then_crash_double_latent,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of set_x_then_crash_double_latent,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference2_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `test_after_dereference2_latent` here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference2_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `test_after_dereference2_latent` here,parameter `x` of test_after_dereference2_latent,invalid access occurs here]
@ -63,6 +64,9 @@ codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE
codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, FP_smart_pointer, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Node::getShared` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Node::getShared`,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,return from call to `Node::getShared`,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, FP_std_value_or_check_value_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, FP_value_or_check_value_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional<int>::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,return from call to `folly::Optional<int>::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional<int>::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,passed as argument to `folly::Optional<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,passed as argument to `folly::Optional<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,assigned,invalid access occurs here]

@ -185,9 +185,7 @@ int value_or_check_empty_ok() {
return -1; return -1;
} }
// missing a more precise model for constructing an optional from a int FP_value_or_check_value_ok() {
// value, which could cause an FP but doesn't at the moment
int value_or_check_value_ok() {
folly::Optional<int> foo{5}; folly::Optional<int> foo{5};
int x = foo.value_or(0); int x = foo.value_or(0);
if (x != 5) { if (x != 5) {
@ -306,7 +304,7 @@ int std_value_or_check_empty_ok() {
return -1; return -1;
} }
int std_value_or_check_value_ok() { int FP_std_value_or_check_value_ok() {
std::optional<int> foo{5}; std::optional<int> foo{5};
int x = foo.value_or(0); int x = foo.value_or(0);
if (x != 5) { if (x != 5) {
@ -400,7 +398,7 @@ struct Node {
} }
}; };
int smart_pointer(const Node& node) { int FP_smart_pointer(const Node& node) {
if (node.getShared().has_value()) { if (node.getShared().has_value()) {
return *(node.getShared().value()); return *(node.getShared().value());
} }

@ -1,12 +1,12 @@
codetoanalyze/objc/pulse/DeallocCalls.m, memory_leak_raii_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `BufferContainer2.init` here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/DeallocCalls.m, memory_leak_raii_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `BufferContainer2.init` here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MallocInObjC.m, leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MallocInObjC.m, leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.call_no_bridge_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `MemoryLeaks.ret_no_bridge` here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.call_no_bridge_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `MemoryLeaks.ret_no_bridge` here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_mutable_leak_bad:, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_mutable_leak_bad:, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_with_rect_leak_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_with_rect_leak_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.no_bridge_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.no_bridge_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 6, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 7, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `objc_blockcaptured_npe_bad_3` here,parameter `x` of objc_blockcaptured_npe_bad_3,invalid access occurs here] codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `objc_blockcaptured_npe_bad_3` here,parameter `x` of objc_blockcaptured_npe_bad_3,invalid access occurs here]
codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here] codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here]

@ -1,4 +1,4 @@
codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]

Loading…
Cancel
Save