From 9177ba8d2005218779570ddcfa274c3fb051c39b Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Mon, 9 Nov 2015 03:00:41 -0800 Subject: [PATCH] Add model for FileChannel.lock() returning not null Reviewed By: jvillard Differential Revision: D2631231 fb-gh-sync-id: e5a3476 --- .../models/java/src/java/nio/channels/FileChannel.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/infer/models/java/src/java/nio/channels/FileChannel.java b/infer/models/java/src/java/nio/channels/FileChannel.java index 6e5cf7791..3650f6d95 100644 --- a/infer/models/java/src/java/nio/channels/FileChannel.java +++ b/infer/models/java/src/java/nio/channels/FileChannel.java @@ -9,7 +9,9 @@ package java.nio.channels; +import com.facebook.infer.models.InferBuiltins; import java.nio.channels.spi.AbstractInterruptibleChannel; +import java.nio.channels.FileLock; public abstract class FileChannel extends AbstractInterruptibleChannel { @@ -23,4 +25,12 @@ public abstract class FileChannel extends AbstractInterruptibleChannel { private String displayName; } + + private native FileLock getFileLock(); + + FileLock lock() { + FileLock f = getFileLock(); + InferBuiltins.assume(f != null); + return f; + } }