From e7d36ed58a8e9ffc13111162f4228d303473aa75 Mon Sep 17 00:00:00 2001
From: Peter O'Hearn <peteroh@fb.com>
Date: Sun, 29 May 2016 17:41:44 -0700
Subject: [PATCH] model of holdsLock

Reviewed By: sblackshear

Differential Revision: D3328363

fbshipit-source-id: 68497b0
---
 infer/models/java/src/java/lang/Thread.java | 38 +++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 infer/models/java/src/java/lang/Thread.java

diff --git a/infer/models/java/src/java/lang/Thread.java b/infer/models/java/src/java/lang/Thread.java
new file mode 100644
index 000000000..e02155ad2
--- /dev/null
+++ b/infer/models/java/src/java/lang/Thread.java
@@ -0,0 +1,38 @@
+/*
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package java.lang;
+
+import com.facebook.infer.models.InferUndefined;
+import com.facebook.infer.models.InferBuiltins;
+
+class Thread implements Runnable {
+
+  public native void run();
+
+  /* This is a coarse model which doesn't. e.g., explicitly
+     keep track of when something has been locked or unlocked.
+     The typical use case for this method, though, is for when
+     you don't know if a lock is held, we simply want that
+     the lock is held to percolate into the post in the true
+     branch, to reason correctly about use of things guarded
+     by the lock afterwards. We can refine this later if need be.
+  */
+
+  public static boolean holdsLock(Object obj) {
+    if (InferUndefined.boolean_undefined()) {
+          InferBuiltins.__set_locked_attribute(obj);
+          return true;
+    } else {
+          return false;
+   }
+
+  }
+
+}