diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 37c5ab2aa..1f985259c 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -26,8 +26,8 @@ module Path : sig val add_call : bool -> t -> Typ.Procname.t -> t -> t (** add a call with its sub-path, the boolean indicates whether the subtrace for the procedure should be included *) - val add_skipped_call : t -> Typ.Procname.t -> string -> t - (** add a call to a procname that's had to be skipped, along with the reason *) + val add_skipped_call : t -> Typ.Procname.t -> string -> Location.t option -> t + (** add a call to a procname that's had to be skipped, along with the reason and the location of the procname when known *) val contains : t -> t -> bool (** check whether a path contains another path *) @@ -99,7 +99,7 @@ end = struct let compare__string_option _ _ = 0 type _path_exec = - | ExecSkipped of string (** call was skipped with a reason *) + | ExecSkipped of string * Location.t option (** call was skipped with a reason *) | ExecCompleted of t (** call was completed *) and t = @@ -153,7 +153,8 @@ end = struct let add_call include_subtrace p pname p_sub = if include_subtrace then Pcall (p, pname, ExecCompleted p_sub, get_dummy_stats ()) else p - let add_skipped_call p pname reason = Pcall (p, pname, ExecSkipped reason, get_dummy_stats ()) + let add_skipped_call p pname reason loc_opt = + Pcall (p, pname, ExecSkipped (reason, loc_opt), get_dummy_stats ()) (** functions in this module either do not assume, or do not re-establish, the invariant on dummy stats *) @@ -419,7 +420,7 @@ end = struct -> F.fprintf fmt "(%a + %a)" (doit (n - 1)) path1 (doit (n - 1)) path2 | Pcall (path1, _, ExecCompleted path2, _) -> F.fprintf fmt "(%a{%a})" (doit (n - 1)) path1 (doit (n - 1)) path2 - | Pcall (path, _, ExecSkipped reason, _) + | Pcall (path, _, ExecSkipped (reason, _), _) -> F.fprintf fmt "(%a: %s)" (doit (n - 1)) path reason in let print_delayed () = @@ -443,13 +444,21 @@ end = struct let trace = ref [] in let g level path _ exn_opt = match (path, curr_node path) with - | Pcall (_, pname, ExecSkipped reason, _), Some curr_node + | Pcall (_, pname, ExecSkipped (reason, loc_opt), _), Some curr_node -> let curr_loc = Procdesc.Node.get_loc curr_node in let descr = Format.sprintf "Skipping %s: %s" (Typ.Procname.to_simplified_string pname) reason in let node_tags = [] in - trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace + trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace ; + Option.iter + ~f:(fun loc -> + if Typ.Procname.is_java pname && loc.Location.line > 0 then + let definition_descr = + Format.sprintf "Definition of %s" (Typ.Procname.to_simplified_string pname) + in + trace := Errlog.make_trace_element (level + 1) loc definition_descr [] :: !trace) + loc_opt | _, Some curr_node -> ( let curr_loc = Procdesc.Node.get_loc curr_node in diff --git a/infer/src/backend/paths.mli b/infer/src/backend/paths.mli index 4625d58a8..f37e383d6 100644 --- a/infer/src/backend/paths.mli +++ b/infer/src/backend/paths.mli @@ -21,8 +21,8 @@ module Path : sig val add_call : bool -> t -> Typ.Procname.t -> t -> t (** add a call with its sub-path, the boolean indicates whether the subtrace for the procedure should be included *) - val add_skipped_call : t -> Typ.Procname.t -> string -> t - (** add a call to a procname that's had to be skipped, along with the reason *) + val add_skipped_call : t -> Typ.Procname.t -> string -> Location.t option -> t + (** add a call to a procname that's had to be skipped, along with the reason and the location of the procname when known *) val contains : t -> t -> bool (** check whether a path contains another path *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 7a8787be9..c98159e90 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1596,7 +1596,12 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots Attribute.mark_vars_as_undefined tenv pre_final ~ret_exp_opt ~undefined_actuals_by_ref callee_pname ret_annots loc path_pos in - let skip_path = Paths.Path.add_skipped_call path callee_pname reason in + let callee_loc_opt = + Option.map + ~f:(fun attributes -> attributes.ProcAttributes.loc) + (Specs.proc_resolve_attributes callee_pname) + in + let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in [(prop_with_undef_attr, skip_path)] and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos) diff --git a/infer/tests/build_systems/buck/issues.exp b/infer/tests/build_systems/buck/issues.exp index 603b0f30f..fe0074f42 100644 --- a/infer/tests/build_systems/buck/issues.exp +++ b/infer/tests/build_systems/buck/issues.exp @@ -1,5 +1,5 @@ infer/tests/build_systems/genrule/module1/Class1.java, void Class1.localNPE1(), 2, NULL_DEREFERENCE, [start of procedure localNPE1()] -infer/tests/build_systems/genrule/module2/Class2.java, void Class2.followMethodDeclarationOnlyBad(SkipImplementationClass1), 2, NULL_DEREFERENCE, [start of procedure followMethodDeclarationOnlyBad(...),Skipping annotatedNullable(): method has no implementation] +infer/tests/build_systems/genrule/module2/Class2.java, void Class2.followMethodDeclarationOnlyBad(SkipImplementationClass1), 2, NULL_DEREFERENCE, [start of procedure followMethodDeclarationOnlyBad(...),Skipping annotatedNullable(): method has no implementation,Definition of annotatedNullable()] infer/tests/build_systems/genrule/module2/Class2.java, void Class2.interTargetAbstractNPE(Class1), 2, NULL_DEREFERENCE, [start of procedure interTargetAbstractNPE(...),Skipping abstractMayReturnNull(): abstract method] infer/tests/build_systems/genrule/module2/Class2.java, void Class2.interTargetNPE(), 2, NULL_DEREFERENCE, [start of procedure interTargetNPE(),start of procedure returnsNull(),return from a call to String Class1.returnsNull()] infer/tests/build_systems/genrule/module2/Class2.java, void Class2.interTargetNativeNPE(Class1), 2, NULL_DEREFERENCE, [start of procedure interTargetNativeNPE(...),Skipping nativeMayReturnNull(): method has no implementation] diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index d85221241..2502e7b64 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -16,7 +16,7 @@ codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipFunctionInLo codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(), 2, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero()] codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(), 2, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...)] codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(), 3, DIVIDE_BY_ZERO, [start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method] -codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 26, DIVIDE_BY_ZERO, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),return from a call to void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...),return from a call to void AnalysisStops.divideByParam(int),return from a call to void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),return from a call to void AnalysisStops.castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),Skipping toString(): unknown method,return from a call to void AnalysisStops.callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,start of procedure retZero(),return from a call to int AnalysisStops$MyObj.retZero(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure retOne(),return from a call to int AnalysisStops$MyObj.retOne(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldWriteOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldWriteOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldReadOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalsePositive(),start of procedure recursiveAngelicTypesMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.recursiveAngelicTypesMayCauseFalseNegative(),Skipping recursiveAngelicTypesMayCauseFalsePositive(): empty list of specs,start of procedure infiniteMaterializationMayCauseFalseNegative(...),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalseNegative(boolean),start of procedure infiniteMaterializationMayCauseFalsePositive(...),Skipping externalFunc2(): method has no implementation,Taking false branch,Skipping toString(): unknown method,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalsePositive(boolean),start of procedure primitiveFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalsePositive(),start of procedure primitiveFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalseNegative(),start of procedure heapFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalsePositive(),start of procedure heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping fieldReadAferCastMayCauseFalseNegative(...): empty list of specs,start of procedure fieldReadInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeMayCauseFalsePositive(),start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),start of procedure accessPathInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure accessPathOnParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.accessPathOnParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.accessPathInCalleeMayCauseFalsePositive()] +codetoanalyze/java/infer/AnalysisStops.java, void AnalysisStops.specInferenceMayFailAndCauseFalseNegative(boolean,Iterator), 26, DIVIDE_BY_ZERO, [start of procedure specInferenceMayFailAndCauseFalseNegative(...),start of procedure skipPointerDerefMayCauseLocalFalseNegative(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.skipPointerDerefMayCauseLocalFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetObj(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to Object AnalysisStops.skipPointerDerefPreventsSpecInferenceRetObj(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),return from a call to void AnalysisStops.skipPointerDerefMayCauseCalleeFalseNegative(),start of procedure skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure skipPointerDerefPreventsSpecInferenceRetZero(),Skipping externalFunc(): method has no implementation,Skipping toString(): unknown method,return from a call to int AnalysisStops.skipPointerDerefPreventsSpecInferenceRetZero(),start of procedure divideByParam(...),return from a call to void AnalysisStops.divideByParam(int),return from a call to void AnalysisStops.skipPointerDerefMayCauseInterprocFalseNegative(),start of procedure castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),return from a call to void AnalysisStops.castFailureOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure castExternalPreventsSpecInference(),return from a call to String AnalysisStops.castExternalPreventsSpecInference(),Skipping toString(): unknown method,return from a call to void AnalysisStops.callOnCastUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,start of procedure retZero(),return from a call to int AnalysisStops$MyObj.retZero(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalseNegative(),start of procedure callOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure retOne(),return from a call to int AnalysisStops$MyObj.retOne(),return from a call to void AnalysisStops.callOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldWriteOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldWriteOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldWriteOnUndefinedObjMayCauseFalsePositive(),start of procedure fieldReadOnUndefinedObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalseNegative(),start of procedure fieldReadOnUndefinedObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Skipping toString(): unknown method,return from a call to void AnalysisStops.fieldReadOnUndefinedObjMayCauseFalsePositive(),start of procedure recursiveAngelicTypesMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,return from a call to void AnalysisStops.recursiveAngelicTypesMayCauseFalseNegative(),Skipping recursiveAngelicTypesMayCauseFalsePositive(): empty list of specs,Definition of recursiveAngelicTypesMayCauseFalsePositive(),start of procedure infiniteMaterializationMayCauseFalseNegative(...),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalseNegative(boolean),start of procedure infiniteMaterializationMayCauseFalsePositive(...),Skipping externalFunc2(): method has no implementation,Taking false branch,Skipping toString(): unknown method,return from a call to void AnalysisStops.infiniteMaterializationMayCauseFalsePositive(boolean),start of procedure primitiveFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalsePositive(),start of procedure primitiveFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.primitiveFieldOfAngelicObjMayCauseFalseNegative(),start of procedure heapFieldOfAngelicObjMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,Taking false branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalsePositive(),start of procedure heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping externalFunc2(): method has no implementation,Taking true branch,return from a call to void AnalysisStops.heapFieldOfAngelicObjMayCauseFalseNegative(),Skipping fieldReadAferCastMayCauseFalseNegative(...): empty list of specs,Definition of fieldReadAferCastMayCauseFalseNegative(...),start of procedure fieldReadInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeMayCauseFalsePositive(),start of procedure fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure derefParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.derefParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive(),start of procedure accessPathInCalleeMayCauseFalsePositive(),Skipping externalFunc2(): method has no implementation,start of procedure accessPathOnParam(...),Skipping toString(): unknown method,return from a call to void AnalysisStops.accessPathOnParam(AnalysisStops$MyObj),return from a call to void AnalysisStops.accessPathInCalleeMayCauseFalsePositive()] codetoanalyze/java/infer/ArrayOutOfBounds.java, int ArrayOutOfBounds.arrayOutOfBounds(), 2, ARRAY_OUT_OF_BOUNDS_L1, [start of procedure arrayOutOfBounds()] codetoanalyze/java/infer/Builtins.java, void Builtins.causeError(Object), 2, NULL_DEREFERENCE, [start of procedure causeError(...),Taking true branch] codetoanalyze/java/infer/Builtins.java, void Builtins.doNotBlockError(Object), 3, NULL_DEREFERENCE, [start of procedure doNotBlockError(...),Taking true branch]