Model and test FileChannel.tryLock throws

Summary: Add possibility of throwing IOException to model of
java.nio.channels.FileChannel.tryLock, and add test case.

public

Reviewed By: cristianoc

Differential Revision: D2658203

fb-gh-sync-id: 9ca9c02

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();
     }
 

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",

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"
   }
 ]

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
+    }
+  }
+
 }

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,