diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 780a4aed2..f47155803 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -404,8 +404,8 @@ let mk_rules_for_dll (para : Sil.hpara_dll) : rule list = (****************** End of DLL abstraction rules ******************) (****************** Start of Predicate Discovery ******************) -let typ_get_recursive_flds tenv te = - let filter (_, t, _) = +let typ_get_recursive_flds tenv typ_exp = + let filter typ (_, t, _) = match t with | Sil.Tvar _ | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ -> false | Sil.Tptr (Sil.Tvar tname', _) -> @@ -414,22 +414,22 @@ let typ_get_recursive_flds tenv te = L.err "@.typ_get_recursive: Undefined type %s@." (Typename.to_string tname'); t | Some typ' -> typ' in - Sil.exp_equal te (Sil.Sizeof (typ', Sil.Subtype.exact)) + Sil.typ_equal typ' typ | Sil.Tptr _ | Sil.Tstruct _ | Sil.Tarray _ | Sil.Tenum _ -> false in - match te with + match typ_exp with | Sil.Sizeof (typ, _) -> (match typ with | Sil.Tvar _ -> assert false (* there should be no indirection *) | Sil.Tint _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tfloat _ | Sil.Tenum _ -> [] | Sil.Tstruct { Sil.instance_fields } -> - IList.map (fun (x, y, z) -> x) (IList.filter filter instance_fields) + IList.map (fun (x, y, z) -> x) (IList.filter (filter typ) instance_fields) | Sil.Tarray _ -> []) | Sil.Var _ -> [] (* type of |-> not known yet *) | Sil.Const _ -> [] | _ -> - L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) te; + L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) typ_exp; assert false let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option = diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 40e6f0054..016cde79f 100644 --- a/infer/tests/ant_report.json +++ b/infer/tests/ant_report.json @@ -229,6 +229,11 @@ "file": "codetoanalyze/java/infer/NullPointerExceptions.java", "procedure": "void NullPointerExceptions.derefNullableGetter()" }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)" + }, { "bug_type": "RESOURCE_LEAK", "file": "codetoanalyze/java/infer/FilterInputStreamLeaks.java", diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json index cb79fb3d0..162bd24cb 100644 --- a/infer/tests/buck_report.json +++ b/infer/tests/buck_report.json @@ -229,6 +229,11 @@ "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", "procedure": "void NullPointerExceptions.derefNullableGetter()" }, + { + "bug_type": "NULL_DEREFERENCE", + "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", + "procedure": "void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)" + }, { "bug_type": "RESOURCE_LEAK", "file": "infer/tests/codetoanalyze/java/infer/FilterInputStreamLeaks.java", diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 303e0b231..c8adfa4f6 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -469,4 +469,20 @@ public class NullPointerExceptions { } } + class L { + L next; + } + + Object returnsNullAfterLoopOnList(L l) { + while (l != null) { + l = l.next; + } + return null; + } + + void dereferenceAfterLoopOnList(L l) { + Object obj = returnsNullAfterLoopOnList(l); + obj.toString(); + } + } diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index 106a6b5e7..52ad0f334 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -67,7 +67,8 @@ public class NullPointerExceptionTest { "derefNull", "nullListFiles", "nullTryLock", - "tryLockThrows" + "tryLockThrows", + "dereferenceAfterLoopOnList", }; assertThat( "Results should contain " + NULL_DEREFERENCE,