diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index e7316135e..878581df0 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1359,6 +1359,7 @@ module ProcNameDispatcher = struct ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "next" <>$ capt_arg_payload $!--> JavaIterator.next ~desc:"Iterator.next()" + ; +match_builtin BuiltinDecl.__instanceof &--> Misc.return_positive ~desc:"instanceof" ; ( +map_context_tenv PatternMatch.Java.implements_enumeration &:: "nextElement" <>$ capt_arg_payload $!--> fun x -> diff --git a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java new file mode 100644 index 000000000..778da668e --- /dev/null +++ b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java @@ -0,0 +1,68 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +public class InstanceOfExample { + abstract class Person {} + + class Faculty extends Person {} + + class Professor extends Faculty {} + + class Student extends Person {} + + public void testInstanceOfObjFacultyOk() { + Person p = new Professor(); + Person p2 = null; + if (p instanceof Faculty) { + p2 = new Student(); + } + p2.toString(); + } + + public Person updatePerson(Person p) { + Person new_p = null; + if (p instanceof Student) { + new_p = p; + } + + if (p instanceof Professor) { + new_p = null; + } + + return new_p; + } + + public void FP_testInstanceOfObjProfessorOk() { + Person p = new Professor(); + if (p instanceof Student) { + String x = updatePerson(p).toString(); + } + } + + public void FP_testInstanceOfObjStudentOk() { + Person p = new Student(); + Person new_p = updatePerson(p); + new_p.toString(); + } + + public Object checkInstanceArray(Object array) { + Object o = null; + if (array instanceof boolean[]) { + o = new Object(); + } + + if (array instanceof int[]) { + o.toString(); + } + + return o; + } + + public void FN_testInstanceOfArrayIntBad() { + int arr[] = new int[10]; + checkInstanceArray(arr); + } +} diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index bdb31f420..4143a5fa6 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -14,6 +14,8 @@ codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicD codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Subtype.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Subtype.foo()`,return from call to `Object DynamicDispatch$Subtype.foo()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicResolutionWithVariadicMethodBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,return from call to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Impl.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Impl.foo()`,return from call to `Object DynamicDispatch$Impl.foo()`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.FP_testInstanceOfObjProfessorOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.FP_testInstanceOfObjStudentOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerBuiltInEqualOperatorCachedValuesOk():void, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodBad():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]