[infer][java] the detection of a resource leak should not prevent the symbolic execution to proceed

Summary:
When detecting a resource leak, Infer used to raise an Leak exception and then prevent the specs to be computed for the paths containing a leak. This diff prevents resource leak to stop the analysis.
master
jrm 9 years ago
parent 9ac4b11056
commit 2dc796542a

@ -1333,8 +1333,8 @@ let check_junk ?original_prop pname tenv prop =
list_mem attr_opt_equal alloc_attribute !leaks_reported in list_mem attr_opt_equal alloc_attribute !leaks_reported in
let ignore_leak = let ignore_leak =
!Config.allowleak || ignore_resource || is_undefined || already_reported () in !Config.allowleak || ignore_resource || is_undefined || already_reported () in
(* in footprint mode, report leak and continue *) let report_and_continue =
let report_and_continue = !Config.footprint in !Sil.curr_language = Sil.Java || !Config.footprint in
let report_leak () = let report_leak () =
if not report_and_continue then raise exn if not report_and_continue then raise exn
else else

@ -16,17 +16,13 @@ import java.io.IOException;
import java.io.StringReader; import java.io.StringReader;
public class CloseableAsResourceExample {
native boolean star();
class LocalException extends IOException { class LocalException extends IOException {
} }
class SomeResource implements Closeable { class SomeResource implements Closeable {
void doSomething() throws LocalException { void doSomething() throws LocalException {
if (!star()) { if (!CloseableAsResourceExample.star()) {
throw new LocalException(); throw new LocalException();
} }
} }
@ -34,6 +30,41 @@ public class CloseableAsResourceExample {
public void close() {} public void close() {}
} }
class Resource implements Closeable {
public Resource() {
}
public void close() {}
}
class Wrapper implements Closeable {
Resource mR;
public Wrapper(Resource r) {
mR = r;
}
public void close() {
mR.close();
}
}
class Sub extends Wrapper {
public Sub(Resource r) {
super(r);
}
}
class ResourceWithException implements Closeable {
public void close() throws IOException {
if (CloseableAsResourceExample.star()) {
throw new IOException();
}
}
}
public class CloseableAsResourceExample {
native static boolean star();
void closingCloseable() { void closingCloseable() {
SomeResource res = new SomeResource(); SomeResource res = new SomeResource();
res.close(); res.close();
@ -59,27 +90,6 @@ public class CloseableAsResourceExample {
res.close(); res.close();
} // should report a resource leak } // should report a resource leak
class Resource implements Closeable {
public Resource() {
}
public void close() {}
}
class Wrapper implements Closeable {
Resource mR;
public Wrapper(Resource r) {
mR = r;
}
public void close() {
mR.close();
}
}
class Sub extends Wrapper {
public Sub(Resource r) {
super(r);
}
}
void closingWrapper() { void closingWrapper() {
Resource r = new Resource(); Resource r = new Resource();
@ -124,15 +134,6 @@ public class CloseableAsResourceExample {
} }
} }
class ResourceWithException implements Closeable {
public void close() throws IOException {
if (star()) {
throw new IOException();
}
}
}
void noLeakwithExceptionOnClose() throws IOException { void noLeakwithExceptionOnClose() throws IOException {
ResourceWithException res = new ResourceWithException(); ResourceWithException res = new ResourceWithException();
res.close(); res.close();
@ -143,4 +144,9 @@ public class CloseableAsResourceExample {
Utils.closeQuietly(res); Utils.closeQuietly(res);
} }
static T sourceOfNullWithResourceLeak() {
SomeResource r = new SomeResource();
return null;
}
} }

@ -335,10 +335,16 @@ public class NullPointerExceptions {
} }
} }
void nullableNonNullStringAfterTextUtilsIsEmptyCheckShouldNotCauseNPE(@Nullable String str) { void nullableNonNullStringAfterTextUtilsIsEmptyCheckShouldNotCauseNPE(@Nullable String str) {
if (!TextUtils.isEmpty(str)) { if (!TextUtils.isEmpty(str)) {
str.length(); str.length();
} }
} }
void someNPEAfterResourceLeak() {
T t = CloseableAsResourceExample.sourceOfNullWithResourceLeak();
t.f();
}
} }

@ -42,6 +42,7 @@ public class CloseableAsResourceTest {
"notClosingCloseable", "notClosingCloseable",
"notClosingWrapper", "notClosingWrapper",
"failToCloseWithCloseQuietly", "failToCloseWithCloseQuietly",
"sourceOfNullWithResourceLeak",
}; };
assertThat( assertThat(
"Results should not contain resource leak errors", "Results should not contain resource leak errors",

@ -59,7 +59,8 @@ public class NullPointerExceptionTest {
"nullableParamNPE", "nullableParamNPE",
"badCheckShouldCauseNPE", "badCheckShouldCauseNPE",
"nullPointerExceptionArrayLength", "nullPointerExceptionArrayLength",
"npeWithDollars" "npeWithDollars",
"someNPEAfterResourceLeak",
}; };
assertThat( assertThat(
"Results should contain " + NULL_DEREFERENCE, "Results should contain " + NULL_DEREFERENCE,

Loading…
Cancel
Save