diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index eb02bdb44..ae9c77a7d 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -1070,17 +1070,7 @@ let instruction (context : JContext.t) pc instr : translation = let call_node = create_node node_kind (instrs @ call_instrs) in call_node in - let trans_virtual_call original_cn invoke_kind = - let cn' = - match JTransType.extract_cn_no_obj sil_obj_type with - | Some cn -> - cn - | None -> - original_cn - in - let call_node = create_call_node cn' invoke_kind in - Instr call_node - in + let trans_virtual_call cn invoke_kind = Instr (create_call_node cn invoke_kind) in match call_kind with | JBir.VirtualCall obj_type -> let cn = diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index f5653d6e0..3f8a4d415 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -71,15 +71,6 @@ let rec create_array_type typ dim = else typ -let extract_cn_no_obj (typ : Typ.t) = - match typ.desc with - | Tptr ({desc= Tstruct (JavaClass _ as name)}, Pk_pointer) -> - let class_name = JBasics.make_cn (Typ.Name.name name) in - if JBasics.cn_equal class_name JBasics.java_lang_object then None else Some class_name - | _ -> - None - - (** Printing types *) let object_type_to_string ot = let rec array_type_to_string (vt : JBasics.value_type) = diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli index df2580c6a..85540502a 100644 --- a/infer/src/java/jTransType.mli +++ b/infer/src/java/jTransType.mli @@ -64,9 +64,5 @@ val package_to_string : string list -> string option val create_array_type : Typ.t -> int -> Typ.t (** [create_array_type typ dim] creates an array type with dimension dim and content typ *) -val extract_cn_no_obj : Typ.t -> JBasics.class_name option -(** [extract_cn_type_np] returns the Java class name of typ when typ is a pointer type, otherwise - returns None *) - val object_type_to_string : JBasics.object_type -> string (** returns a string representation of an object Java type *) diff --git a/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java b/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java index ae23b0d73..6d9ad5c22 100644 --- a/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java +++ b/infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java @@ -34,7 +34,7 @@ public class ReaderLeaks { } } - public void readerClosed() throws IOException { + public void readerClosed_FP() throws IOException { Reader r = null; try { r = new FileReader("testing.txt"); diff --git a/infer/tests/codetoanalyze/java/biabduction/issues.exp b/infer/tests/codetoanalyze/java/biabduction/issues.exp index 3b2459e48..56d6c5f7e 100644 --- a/infer/tests/codetoanalyze/java/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/java/biabduction/issues.exp @@ -137,6 +137,7 @@ codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.Reader codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pipedReaderNotClosedAfterConnect(java.io.PipedWriter):void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pipedReaderNotClosedAfterConnect(...),exception java.io.IOException] codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pipedReaderNotClosedAfterConstructedWithWriter():void, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pipedReaderNotClosedAfterConstructedWithWriter(),exception java.io.IOException] codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pushbackReaderNotClosedAfterRead():void, 6, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pushbackReaderNotClosedAfterRead(),Skipping PushbackReader(...): unknown method,exception java.io.IOException] +codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.readerClosed_FP():void, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure readerClosed_FP(),Skipping FileReader(...): unknown method,exception java.io.IOException,Switch condition is true. Entering switch case,Taking true branch] codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.readerNotClosedAfterRead():void, 6, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure readerNotClosedAfterRead(),Skipping FileReader(...): unknown method,exception java.io.IOException] codetoanalyze/java/biabduction/ResourceLeaks.java, codetoanalyze.java.infer.ResourceLeaks.NoResourceLeakWarningAfterCheckState(java.io.File,int):void, 2, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure NoResourceLeakWarningAfterCheckState(...),Taking false branch] codetoanalyze/java/biabduction/ResourceLeaks.java, codetoanalyze.java.infer.ResourceLeaks.activityObtainTypedArrayAndLeak(android.app.Activity):void, 2, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure activityObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(TypedArray)] diff --git a/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java b/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java index fdc9cd6c3..dd4352bbc 100644 --- a/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java +++ b/infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java @@ -45,23 +45,19 @@ public class DefaultInInterface { } } - static void FN_uncertainCallNPE(int i) { - A firstAthenB = new A(); + static void uncertainCallMethod1NPE(int i) { + A aAorB = new A(); if (i > 0) { // feasible path - firstAthenB = new B(); + aAorB = new B(); } - System.out.println(firstAthenB.defaultMethod1().toString()); + System.out.println(aAorB.defaultMethod1().toString()); } - static boolean alwaysFalse() { - return false; - } - - static void FP_uncertainCallOk(int i) { - A firstAthenB = new A(); - if (alwaysFalse()) { // unfeasible path - firstAthenB = new B(); + static void FN_uncertainCallMethod2NPE(int i) { + A aAorB = new A(); + if (i > 0) { // feasible path + aAorB = new B(); } - System.out.println(firstAthenB.defaultMethod2().toString()); + System.out.println(aAorB.defaultMethod2().toString()); } } diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 56a49b69c..7509df621 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -1,6 +1,6 @@ codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$A.defaultCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$B.overridenCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here] -codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.FP_uncertainCallOk(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Supertype.bar()`,return from call to `Object DynamicDispatch$Supertype.bar()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]