[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

@@ -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

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

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]

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<lol>(): 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<lol>(): 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<lol>(): 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<lol>(): 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]

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<lol>();
   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<lol>();
   skip_const2(0, foo, 0, 0);
   test_pointer(foo);

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<Object> 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

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]

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.<init>(),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.<init>(),return from a call to SubClassA.<init>(),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.<init>(),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()]