diff --git a/infer/models/java/src/java/nio/channels/FileChannel.java b/infer/models/java/src/java/nio/channels/FileChannel.java index 92168d1f7..e96a77505 100644 --- a/infer/models/java/src/java/nio/channels/FileChannel.java +++ b/infer/models/java/src/java/nio/channels/FileChannel.java @@ -11,6 +11,7 @@ package java.nio.channels; import com.facebook.infer.models.InferUndefined; import javax.annotation.Nullable; +import java.io.IOException; import java.nio.channels.spi.AbstractInterruptibleChannel; import java.nio.channels.FileLock; @@ -27,7 +28,8 @@ public abstract class FileChannel extends AbstractInterruptibleChannel { private String displayName; } - public @Nullable FileLock tryLock() { + @Nullable FileLock tryLock() throws IOException { + InferUndefined.can_throw_ioexception_object(); if (InferUndefined.boolean_undefined()) { return null; } else { @@ -35,7 +37,7 @@ public abstract class FileChannel extends AbstractInterruptibleChannel { } } - public final @Nullable FileLock tryLock(long position, long size, boolean shared) { + @Nullable FileLock tryLock(long position, long size, boolean shared) throws IOException { return tryLock(); } diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 307c5f2b6..adf0de3e1 100644 --- a/infer/tests/ant_report.json +++ b/infer/tests/ant_report.json @@ -364,6 +364,11 @@ "file": "codetoanalyze/java/infer/NullPointerExceptions.java", "bug_type": "NULL_DEREFERENCE" }, + { + "procedure": "String NullPointerExceptions.tryLockThrows(FileChannel)", + "file": "codetoanalyze/java/infer/NullPointerExceptions.java", + "bug_type": "NULL_DEREFERENCE" + }, { "procedure": "void ReaderLeaks.readerNotClosedAfterRead()", "file": "codetoanalyze/java/infer/ReaderLeaks.java", diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json index 1b055eb9d..a42b6c002 100644 --- a/infer/tests/buck_report.json +++ b/infer/tests/buck_report.json @@ -723,5 +723,10 @@ "procedure": "void ResourceLeaks.jarInputStreamLeak()", "file": "infer/tests/codetoanalyze/java/infer/ResourceLeaks.java", "bug_type": "RESOURCE_LEAK" + }, + { + "procedure": "String NullPointerExceptions.tryLockThrows(FileChannel)", + "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", + "bug_type": "NULL_DEREFERENCE" } ] \ No newline at end of file diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 7a24ee87f..1abd21869 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -459,4 +459,14 @@ public class NullPointerExceptions { return lock.toString(); // expect possible NullPointerException as lock == null is possible } + String tryLockThrows(FileChannel chan) { + try { + FileLock lock = chan.tryLock(); + return (lock != null ? lock.toString() : ""); + } catch (IOException _) { + Object o = null; + return o.toString(); // expect NullPointerException as tryLock can throw + } + } + } diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index 39dd6eb45..544b3781a 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -66,7 +66,8 @@ public class NullPointerExceptionTest { "testSystemGetPropertyReturn", "derefNull", "nullListFiles", - "nullTryLock" + "nullTryLock", + "tryLockThrows" }; assertThat( "Results should contain " + NULL_DEREFERENCE,