diff --git a/infer/models/java/src/java/nio/channels/FileChannel.java b/infer/models/java/src/java/nio/channels/FileChannel.java index 10bab86da..92168d1f7 100644 --- a/infer/models/java/src/java/nio/channels/FileChannel.java +++ b/infer/models/java/src/java/nio/channels/FileChannel.java @@ -9,7 +9,8 @@ package java.nio.channels; -import com.facebook.infer.models.InferBuiltins; +import com.facebook.infer.models.InferUndefined; +import javax.annotation.Nullable; import java.nio.channels.spi.AbstractInterruptibleChannel; import java.nio.channels.FileLock; @@ -26,6 +27,16 @@ public abstract class FileChannel extends AbstractInterruptibleChannel { private String displayName; } - private native FileLock getFileLock(); + public @Nullable FileLock tryLock() { + if (InferUndefined.boolean_undefined()) { + return null; + } else { + return (FileLock)InferUndefined.object_undefined(); + } + } + + public final @Nullable FileLock tryLock(long position, long size, boolean shared) { + return tryLock(); + } } diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 977ea3cc6..307c5f2b6 100644 --- a/infer/tests/ant_report.json +++ b/infer/tests/ant_report.json @@ -359,6 +359,11 @@ "file": "codetoanalyze/java/infer/NullPointerExceptions.java", "bug_type": "NULL_DEREFERENCE" }, + { + "procedure": "String NullPointerExceptions.nullTryLock(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 f41b918ae..1b055eb9d 100644 --- a/infer/tests/buck_report.json +++ b/infer/tests/buck_report.json @@ -559,6 +559,11 @@ "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", "bug_type": "NULL_DEREFERENCE" }, + { + "procedure": "String NullPointerExceptions.nullTryLock(FileChannel)", + "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java", + "bug_type": "NULL_DEREFERENCE" + }, { "procedure": "void ContextLeaks.directLeak()", "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 3a5743125..7a24ee87f 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -24,6 +24,8 @@ import java.io.File; import java.io.FileInputStream; import java.io.FileOutputStream; import java.io.IOException; +import java.nio.channels.FileChannel; +import java.nio.channels.FileLock; import java.lang.System; import java.util.HashMap; @@ -452,4 +454,9 @@ public class NullPointerExceptions { o.toString(); } + String nullTryLock(FileChannel chan) throws IOException { + FileLock lock = chan.tryLock(); + return lock.toString(); // expect possible NullPointerException as lock == null is possible + } + } diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index 31c435c79..39dd6eb45 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -65,7 +65,8 @@ public class NullPointerExceptionTest { "testSystemGetPropertyArgument", "testSystemGetPropertyReturn", "derefNull", - "nullListFiles" + "nullListFiles", + "nullTryLock" }; assertThat( "Results should contain " + NULL_DEREFERENCE,