diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 9af6014d9..d260cc19f 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -824,9 +824,8 @@ let check_inconsistency_base prop = Sil.pvar_is_seed pv | _ -> false in list_exists do_hpred sigma in - let inconsistent_self () = (* "self" cannot be null in ObjC, outside of initializers *) + let inconsistent_self () = (* "self" cannot be null in ObjC *) let procdesc = Cfg.Node.get_proc_desc (State.get_node ()) in - let procname = Cfg.Procdesc.get_proc_name procdesc in let procedure_attr = Cfg.Procdesc.get_attributes procdesc in let do_hpred = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> @@ -834,8 +833,7 @@ let check_inconsistency_base prop = Sil.exp_equal e Sil.exp_zero && Sil.pvar_is_seed pv && Sil.pvar_get_name pv = Mangled.from_string "self" && - procedure_attr.ProcAttributes.is_objc_instance_method && - not (Procname.is_constructor procname) + procedure_attr.ProcAttributes.is_objc_instance_method | _ -> false in list_exists do_hpred sigma in let inconsistent_atom = function diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index ebbf8e484..d3d4be075 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -788,13 +788,6 @@ let handle_special_cases_call tenv cfg pname actual_params = else pname, actual_params let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc callee_pname loc path = - let receiver_self receiver prop = - list_exists (fun hpred -> - match hpred with - | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> - Sil.exp_equal e receiver && Sil.pvar_is_seed pv && - Sil.pvar_get_name pv = Mangled.from_string "self" - | _ -> false) (Prop.get_sigma prop) in let path_description = "Message "^(Procname.to_simplified_string callee_pname)^" with receiver nil returns nil." in let receiver = (match actual_pars with | (e, _):: _ -> e @@ -804,10 +797,6 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc match actual_pars with | (e, _):: _ when Sil.exp_equal e Sil.exp_zero || Option.is_some (Prop.get_objc_null_attribute pre e) -> true | _ -> false in - let prop_null = - match ret_ids with - | [ret_id] -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero pre - | _ -> pre in let add_objc_null_attribute_or_nullify_result prop = match ret_ids with | [ret_id] -> @@ -830,17 +819,12 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc | _ -> false in if !Config.footprint && not is_undef then let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *) - let is_receiver_self = receiver_self receiver pre in - let pre_with_attr_or_null = - if is_receiver_self then prop_null - else add_objc_null_attribute_or_nullify_result pre in + let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in let propset = prune_ne tenv false receiver Sil.exp_zero pre_with_attr_or_null in if Propset.is_empty propset then [] else let prop = list_hd (Propset.to_proplist propset) in - let path = - if is_receiver_self then path - else Paths.Path.add_description path path_description in + let path = Paths.Path.add_description path path_description in [(prop, path)] in res_null @ res else res (* Not known if receiver = 0 and not footprint. Standard tabulation *) diff --git a/infer/tests/endtoend/objc/NPESelfTest.java b/infer/tests/endtoend/objc/NPESelfTest.java index 777277acb..69054ddf2 100644 --- a/infer/tests/endtoend/objc/NPESelfTest.java +++ b/infer/tests/endtoend/objc/NPESelfTest.java @@ -64,8 +64,8 @@ public class NPESelfTest { throws InterruptedException, IOException, InferException { InferResults inferResults = InferRunner.runInferObjC(inferCmdNPD); assertThat( - "NPE should be found", inferResults, - contains( + "NPE should not be found", inferResults, + doesNotContain( NULL_DEREFERENCE, NPE_FILE, "init"));