From a7e6ba7b2b3b01cfe1bfd4dd0595a54c410c5bbd Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 26 Sep 2017 13:41:54 -0700 Subject: [PATCH] [infer][java] add support for @Nonnull on skipped functions Summary: This diff does two things: # Infer no longer add the contrains that the return value of a skip function is never null. This was leading to false negatives and is not necessary as those return value are treated angelically # Infer now support `Nonnull` on the return value of skip functions. Reviewed By: jberdine, sblackshear Differential Revision: D5840324 fbshipit-source-id: bbd8d82 --- infer/src/backend/rearrange.ml | 2 +- infer/src/backend/symExec.ml | 11 +++--- infer/tests/build_systems/ant/issues.exp | 2 ++ .../tests/codetoanalyze/cpp/errors/issues.exp | 2 ++ .../npe/skip_function_with_const_formals.cpp | 4 +-- .../java/infer/NullPointerExceptions.java | 36 +++++++++++++------ .../tests/codetoanalyze/java/infer/issues.exp | 3 ++ .../codetoanalyze/java/tracing/issues.exp | 5 ++- 8 files changed, 45 insertions(+), 20 deletions(-) diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 04de8f720..5a6a1a3dc 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -1503,7 +1503,7 @@ let is_only_pt_by_fld_or_param_with_annot ?(check_weak_captured_var= false) pdes | Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp ((Exp.Var _ as exp), _), _) when Exp.equal exp deref_exp -> let var_has_annotation = - var_has_annotation ~check_weak_captured_var pdesc is_annotation pvar + Pvar.is_seed pvar && var_has_annotation ~check_weak_captured_var pdesc is_annotation pvar in if var_has_annotation then obj_str := Some (Pvar.to_string pvar) ; let procname_str_opt = attr_has_annot is_annotation tenv prop exp in diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 4b1808c26..a28a2f800 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -912,7 +912,7 @@ let add_struct_value_to_footprint tenv abduced_pv typ prop = let prop' = add_strexp_to_footprint tenv struct_strexp abduced_pv typ prop in (prop', struct_strexp) -let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ callee_pname +let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ callee_pname callee_loc = if Typ.Procname.is_infer_undefined callee_pname then prop else @@ -942,10 +942,9 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca in (* To avoid obvious false positives, assume skip functions do not return null pointers *) let add_ret_non_null exp typ prop = - if has_nullable_annot then prop - (* don't assume nonnull if the procedure is annotated with @Nullable *) - else + if has_nonnull_annot then match typ.Typ.desc with Typ.Tptr _ -> Prop.conjoin_neq tenv exp Exp.zero prop | _ -> prop + else prop in if not (is_rec_call callee_pname) then (* introduce a fresh program variable to allow abduction on the return value *) @@ -1550,7 +1549,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots -> None) args in - let has_nullable_annot = Annotations.ia_is_nullable ret_annots in + let has_nonnull_annot = Annotations.ia_is_nonnull ret_annots in let pre_final = (* in Java, assume that skip functions close resources passed as params *) let pre_1 = if Typ.Procname.is_java callee_pname then remove_file_attribute pre else pre in @@ -1558,7 +1557,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots match (ret_id, ret_type_option) with | Some (ret_id, _), Some ret_typ -> (* TODO(jjb): Should this use the type of ret_id, or ret_type from the procedure type? *) - add_constraints_on_retval tenv pdesc pre_1 (Exp.Var ret_id) ret_typ ~has_nullable_annot + add_constraints_on_retval tenv pdesc pre_1 (Exp.Var ret_id) ret_typ ~has_nonnull_annot callee_pname loc | _ -> pre_1 diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index 9f7a71575..6e2e80650 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -99,6 +99,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions$ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions$E.dereferenceNullableInterfaceFieldBad(), 1, NULL_DEREFERENCE, [start of procedure dereferenceNullableInterfaceFieldBad()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.badCheckShouldCauseNPE(), 1, NULL_DEREFERENCE, [start of procedure badCheckShouldCauseNPE(),start of procedure getBool(),Taking true branch,return from a call to Boolean NullPointerExceptions.getBool(),Taking true branch,start of procedure getObj(),Taking false branch,return from a call to Object NullPointerExceptions.getObj()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.cursorFromContentResolverNPE(String), 9, NULL_DEREFERENCE, [start of procedure cursorFromContentResolverNPE(...)] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.deferenceNullableMethodCallingSkippedMethodBad(), 1, NULL_DEREFERENCE, [start of procedure deferenceNullableMethodCallingSkippedMethodBad(),start of procedure wrapUnknownFuncWithNullable(),return from a call to Object NullPointerExceptions.wrapUnknownFuncWithNullable()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNull(), 2, NULL_DEREFERENCE, [start of procedure derefNull(),start of procedure derefUndefinedCallee(),start of procedure retUndefined(),return from a call to Object NullPointerExceptions.retUndefined(),Skipping toString(): unknown method,return from a call to Object NullPointerExceptions.derefUndefinedCallee()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNullableGetter(), 2, NULL_DEREFERENCE, [start of procedure derefNullableGetter(),start of procedure nullableGetter(),return from a call to Object NullPointerExceptions.nullableGetter()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNullableRet(boolean), 2, NULL_DEREFERENCE, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)] @@ -107,6 +108,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L), 2, NULL_DEREFERENCE, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock1(Lock), 4, NULL_DEREFERENCE, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock2(Lock), 6, NULL_DEREFERENCE, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullDerefernceReturnOfSkippedFunctionBad(), 3, NULL_DEREFERENCE, [start of procedure nullDerefernceReturnOfSkippedFunctionBad(),Skipping unknownFunc(): method has no implementation,Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionArrayLength(), 2, NULL_DEREFERENCE, [start of procedure nullPointerExceptionArrayLength()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionCallArrayReadMethod(), 2, NULL_DEREFERENCE, [start of procedure nullPointerExceptionCallArrayReadMethod(),start of procedure arrayReadShouldNotCauseSymexMemoryError(...),Skipping toString(): unknown method,return from a call to Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index aaa7f0bca..cce567224 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -76,6 +76,8 @@ codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe, 2 codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe_person, 2, NULL_DEREFERENCE, [start of procedure npe_added_to_b1::causes_npe_person(),start of procedure Person,return from a call to npe_added_to_b1::Person_Person,start of procedure npe_added_to_b1::deref_person()] codetoanalyze/cpp/errors/npe/null_returned_by_method.cpp, testNullDeref, 3, NULL_DEREFERENCE, [start of procedure testNullDeref(),Condition is true,start of procedure getNull,return from a call to XFactory_getNull] codetoanalyze/cpp/errors/npe/object_deref.cpp, object_deref::derefNullField, 2, NULL_DEREFERENCE, [start of procedure object_deref::derefNullField(),start of procedure object_deref::getNull(),return from a call to object_deref::getNull] +codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, FP_const_skip2_then_split_case_ok, 4, NULL_DEREFERENCE, [start of procedure FP_const_skip2_then_split_case_ok(),Skipping std::make_shared(): function or method not found,Skipping skip_const2(): function or method not found,start of procedure test_pointer(),Condition is false,return from a call to test_pointer] +codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, FP_const_skip_then_split_case_ok, 5, NULL_DEREFERENCE, [start of procedure FP_const_skip_then_split_case_ok(),Skipping std::make_shared(): function or method not found,Skipping skip_const(): function or method not found,start of procedure test_pointer(),Condition is false,return from a call to test_pointer] codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, FP_typedef_skip_then_split_case_ok, 4, NULL_DEREFERENCE, [start of procedure FP_typedef_skip_then_split_case_ok(),Skipping std::make_shared(): function or method not found,Skipping skip_typedef(): function or method not found,start of procedure test_pointer(),Condition is false,return from a call to test_pointer] codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, skip_then_split_case_bad, 5, NULL_DEREFERENCE, [start of procedure skip_then_split_case_bad(),Skipping std::make_shared(): function or method not found,Skipping skip_no_const(): function or method not found,start of procedure test_pointer(),Condition is false,return from a call to test_pointer] codetoanalyze/cpp/errors/numeric/min_max.cpp, max_X_inv_div0, 2, DIVIDE_BY_ZERO, [start of procedure max_X_inv_div0(),start of procedure X_inv,return from a call to X_inv_X_inv,start of procedure X_inv,return from a call to X_inv_X_inv] diff --git a/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp b/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp index 037369b2c..da5961341 100644 --- a/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp @@ -35,7 +35,7 @@ void skip_then_split_case_bad() { foo->f = 12; // error } -void const_skip_then_split_case_ok() { +void FP_const_skip_then_split_case_ok() { auto foo = std::make_shared(); skip_const(foo); // Infer shouldn't havoc foo here since it's const... test_pointer(foo); /* ...so foo cannot be null here, even if there is an @@ -44,7 +44,7 @@ void const_skip_then_split_case_ok() { } // same as above but make sure infer pinpoints the correct const argument -void const_skip2_then_split_case_ok() { +void FP_const_skip2_then_split_case_ok() { auto foo = std::make_shared(); skip_const2(0, foo, 0, 0); test_pointer(foo); diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 2fe1d1e14..c403833d8 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -22,6 +22,7 @@ import com.google.common.base.Optional; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; +import javax.annotation.Nonnull; import javax.annotation.Nullable; import java.io.File; @@ -175,7 +176,7 @@ public class NullPointerExceptions { } } - public void noNullPointerExceptionAfterSkipFunction() { + public void FP_noNullPointerExceptionAfterSkipFunction() { String t = new String("Hello!"); String s = t.toString(); genericMethodSomewhereCheckingForNull(s); @@ -201,13 +202,6 @@ public class NullPointerExceptions { return h.get(position); } - static void ReturnedValueOfImmutableListOf() { - ImmutableList l = ImmutableList.of(); - if (l == null) { - l.toString(); - } - } - void nullPointerExceptionInArrayLengthLoop(Object[] arr) { for (int i = 0; i < arr.length; i++) { Object x = null; @@ -343,7 +337,6 @@ public class NullPointerExceptions { } } - void nullableNonNullStringAfterTextUtilsIsEmptyCheckShouldNotCauseNPE(@Nullable String str) { if (!TextUtils.isEmpty(str)) { str.length(); @@ -455,7 +448,6 @@ public class NullPointerExceptions { return 3; } - public void testNullablePrecision() { Object ret = undefNullableRet(); if (returnsThreeOnlyIfRetNotNull(ret) == 3) { @@ -507,6 +499,22 @@ public class NullPointerExceptions { native Object unknownFunc(); + void nullDerefernceReturnOfSkippedFunctionBad() { + Object object = unknownFunc(); + if (object == null) { + object.toString(); + } + } + + native @Nonnull Object doesNotReturnNull(); + + void noNPEWhenCallingSkippedNonnullAnnotatedMethodGood() { + Object object = doesNotReturnNull(); + if (object == null) { + object.toString(); + } + } + Object callUnknownFunc() { return unknownFunc(); } @@ -521,6 +529,14 @@ public class NullPointerExceptions { o.toString(); } + @Nullable Object wrapUnknownFuncWithNullable() { + return unknownFunc(); + } + + void deferenceNullableMethodCallingSkippedMethodBad() { + wrapUnknownFuncWithNullable().toString(); + } + String nullTryLock(FileChannel chan) throws IOException { FileLock lock = chan.tryLock(); return lock.toString(); // expect possible NullPointerException as lock == null is possible diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 7f4f3f9c8..90e9658d5 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -124,8 +124,10 @@ codetoanalyze/java/infer/NullPointerExceptions.java, int NullPointerExceptions.n codetoanalyze/java/infer/NullPointerExceptions.java, int NullPointerExceptions.preconditionCheckStateTest(NullPointerExceptions$D), 1, PRECONDITION_NOT_MET, [start of procedure preconditionCheckStateTest(...),Taking false branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars(), 2, NULL_DEREFERENCE, [start of procedure npeWithDollars()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions$E.dereferenceNullableInterfaceFieldBad(), 1, NULL_DEREFERENCE, [start of procedure dereferenceNullableInterfaceFieldBad()] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.FP_noNullPointerExceptionAfterSkipFunction(), 4, NULL_DEREFERENCE, [start of procedure FP_noNullPointerExceptionAfterSkipFunction(),Skipping String(...): unknown method,Skipping toString(): unknown method,start of procedure genericMethodSomewhereCheckingForNull(...),Taking true branch,return from a call to void NullPointerExceptions.genericMethodSomewhereCheckingForNull(String)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.badCheckShouldCauseNPE(), 1, NULL_DEREFERENCE, [start of procedure badCheckShouldCauseNPE(),start of procedure getBool(),Taking true branch,return from a call to Boolean NullPointerExceptions.getBool(),Taking true branch,start of procedure getObj(),Taking false branch,return from a call to Object NullPointerExceptions.getObj()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.cursorFromContentResolverNPE(String), 9, NULL_DEREFERENCE, [start of procedure cursorFromContentResolverNPE(...)] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.deferenceNullableMethodCallingSkippedMethodBad(), 1, NULL_DEREFERENCE, [start of procedure deferenceNullableMethodCallingSkippedMethodBad(),start of procedure wrapUnknownFuncWithNullable(),return from a call to Object NullPointerExceptions.wrapUnknownFuncWithNullable()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNull(), 2, NULL_DEREFERENCE, [start of procedure derefNull(),start of procedure derefUndefinedCallee(),start of procedure retUndefined(),return from a call to Object NullPointerExceptions.retUndefined(),Skipping toString(): unknown method,return from a call to Object NullPointerExceptions.derefUndefinedCallee()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNullableGetter(), 2, NULL_DEREFERENCE, [start of procedure derefNullableGetter(),start of procedure nullableGetter(),return from a call to Object NullPointerExceptions.nullableGetter()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNullableRet(boolean), 2, NULL_DEREFERENCE, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)] @@ -134,6 +136,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L), 2, NULL_DEREFERENCE, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock1(Lock), 4, NULL_DEREFERENCE, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock2(Lock), 6, NULL_DEREFERENCE, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullDerefernceReturnOfSkippedFunctionBad(), 3, NULL_DEREFERENCE, [start of procedure nullDerefernceReturnOfSkippedFunctionBad(),Skipping unknownFunc(): method has no implementation,Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionArrayLength(), 2, NULL_DEREFERENCE, [start of procedure nullPointerExceptionArrayLength()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionCallArrayReadMethod(), 2, NULL_DEREFERENCE, [start of procedure nullPointerExceptionCallArrayReadMethod(),start of procedure arrayReadShouldNotCauseSymexMemoryError(...),Skipping toString(): unknown method,return from a call to Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] diff --git a/infer/tests/codetoanalyze/java/tracing/issues.exp b/infer/tests/codetoanalyze/java/tracing/issues.exp index 8c28ad412..68c89dea7 100644 --- a/infer/tests/codetoanalyze/java/tracing/issues.exp +++ b/infer/tests/codetoanalyze/java/tracing/issues.exp @@ -2,6 +2,7 @@ codetoanalyze/java/infer/ArrayOutOfBounds.java, int ArrayOutOfBounds.arrayOutOfB codetoanalyze/java/infer/ArrayOutOfBounds.java, void ArrayOutOfBounds.switchedArrsOutOfBounds(), 2, java.lang.ArrayIndexOutOfBoundsException, [start of procedure switchedArrsOutOfBounds(),start of procedure buggyIter(...),Taking true branch,Taking false branch,return from a call to void ArrayOutOfBounds.buggyIter(int[],int[]),return from a call to void ArrayOutOfBounds.switchedArrsOutOfBounds()] codetoanalyze/java/infer/ClassCastExceptions.java, int ClassCastExceptions.classCastExceptionImplementsInterface(), 0, java.lang.ClassCastException, [start of procedure classCastExceptionImplementsInterface(),start of procedure AnotherImplementationOfInterface(),return from a call to AnotherImplementationOfInterface.(),start of procedure classCastExceptionImplementsInterfaceCallee(...),Skipping ClassCastException(): unknown method,exception java.lang.ClassCastException,return from a call to int ClassCastExceptions.classCastExceptionImplementsInterfaceCallee(AnotherImplementationOfInterface),exception java.lang.ClassCastException,return from a call to int ClassCastExceptions.classCastExceptionImplementsInterface()] codetoanalyze/java/infer/ClassCastExceptions.java, void ClassCastExceptions.classCastException(), 3, java.lang.ClassCastException, [start of procedure classCastException(),start of procedure SubClassA(),start of procedure SuperClass(),return from a call to SuperClass.(),return from a call to SubClassA.(),Skipping ClassCastException(): unknown method,exception java.lang.ClassCastException,return from a call to void ClassCastExceptions.classCastException()] +codetoanalyze/java/infer/NullPointerExceptions.java, Object NullPointerExceptions.derefUndefinedCallee(), 3, java.lang.NullPointerException, [start of procedure derefUndefinedCallee(),start of procedure retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.derefUndefinedCallee()] codetoanalyze/java/infer/NullPointerExceptions.java, String NullPointerExceptions.testSystemGetPropertyArgument(), 1, NULL_DEREFERENCE, [start of procedure testSystemGetPropertyArgument()] codetoanalyze/java/infer/NullPointerExceptions.java, int NullPointerExceptions.nullListFiles(String), 3, java.lang.NullPointerException, [start of procedure nullListFiles(...),Skipping File(...): unknown method,Taking true branch,exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullListFiles(String)] codetoanalyze/java/infer/NullPointerExceptions.java, int NullPointerExceptions.nullPointerException(), 2, java.lang.NullPointerException, [start of procedure nullPointerException(),exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerException()] @@ -13,8 +14,9 @@ codetoanalyze/java/infer/NullPointerExceptions.java, int NullPointerExceptions.n codetoanalyze/java/infer/NullPointerExceptions.java, int NullPointerExceptions.preconditionCheckStateTest(NullPointerExceptions$D), 1, PRECONDITION_NOT_MET, [start of procedure preconditionCheckStateTest(...),Taking false branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars(), 3, java.lang.NullPointerException, [start of procedure npeWithDollars(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.badCheckShouldCauseNPE(), 2, java.lang.NullPointerException, [start of procedure badCheckShouldCauseNPE(),start of procedure getBool(),Taking true branch,return from a call to Boolean NullPointerExceptions.getBool(),Taking true branch,start of procedure getObj(),Taking true branch,return from a call to Object NullPointerExceptions.getObj(),Taking true branch,return from a call to void NullPointerExceptions.badCheckShouldCauseNPE()] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.deferenceNullableMethodCallingSkippedMethodBad(), 2, java.lang.NullPointerException, [start of procedure deferenceNullableMethodCallingSkippedMethodBad(),start of procedure wrapUnknownFuncWithNullable(),return from a call to Object NullPointerExceptions.wrapUnknownFuncWithNullable(),Taking true branch,return from a call to void NullPointerExceptions.deferenceNullableMethodCallingSkippedMethodBad()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNonThisGetterAfterCheckShouldNotCauseNPE(), 5, java.lang.NullPointerException, [start of procedure derefNonThisGetterAfterCheckShouldNotCauseNPE(),start of procedure NullPointerExceptions(),return from a call to NullPointerExceptions.(),Taking true branch,start of procedure getObj(),Taking true branch,return from a call to Object NullPointerExceptions.getObj(),Taking true branch,Taking true branch,start of procedure getObj(),Taking true branch,return from a call to Object NullPointerExceptions.getObj(),Taking true branch,return from a call to void NullPointerExceptions.derefNonThisGetterAfterCheckShouldNotCauseNPE()] -codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNull(), 3, java.lang.NullPointerException, [start of procedure derefNull(),start of procedure derefUndefinedCallee(),start of procedure retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.derefUndefinedCallee(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.derefNull()] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefNull(), 3, java.lang.NullPointerException, [start of procedure derefNull(),start of procedure derefUndefinedCallee(),start of procedure retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.retUndefined(),exception java.lang.NullPointerException,return from a call to Object NullPointerExceptions.derefUndefinedCallee(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.derefNull()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.derefUndefNullableRetWrapper(), 2, java.lang.NullPointerException, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),return from a call to Object NullPointerExceptions.undefNullableWrapper(),Taking true branch,return from a call to void NullPointerExceptions.derefUndefNullableRetWrapper()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L), 3, java.lang.NullPointerException, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L), 3, java.lang.NullPointerException, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)] @@ -22,6 +24,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock1(Lock), 5, java.lang.NullPointerException, [start of procedure dereferenceAfterUnlock1(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock1(Lock)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock2(Lock), 7, java.lang.NullPointerException, [start of procedure dereferenceAfterUnlock2(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock2(Lock)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dereferenceAfterUnlock2(Lock), 7, java.lang.NullPointerException, [start of procedure dereferenceAfterUnlock2(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock2(Lock)] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.dontReportOnNullableIndirectReassignmentToUnknown(Object), 3, java.lang.NullPointerException, [start of procedure dontReportOnNullableIndirectReassignmentToUnknown(...),start of procedure callUnknownFunc(),return from a call to Object NullPointerExceptions.callUnknownFunc(),Taking true branch,return from a call to void NullPointerExceptions.dontReportOnNullableIndirectReassignmentToUnknown(Object)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionArrayLength(), 3, java.lang.NullPointerException, [start of procedure nullPointerExceptionArrayLength(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionArrayLength()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionCallArrayReadMethod(), 3, java.lang.NullPointerException, [start of procedure nullPointerExceptionCallArrayReadMethod(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionCallArrayReadMethod()] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionCallArrayReadMethod(), 3, java.lang.NullPointerException, [start of procedure nullPointerExceptionCallArrayReadMethod(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionCallArrayReadMethod()]