From 64ab959486a45484796f9020cb5da280f9432aa9 Mon Sep 17 00:00:00 2001
From: Jeremy Dubreil <jrm@fb.com>
Date: Tue, 16 May 2017 21:45:26 -0700
Subject: [PATCH] [infer][java] model the Eradicate assertion utils for the
 biabduction analysis

Summary: Useful to have Eradicate and Biabduction agree on how to inform that the analysis that some objects are not null.

Reviewed By: sblackshear

Differential Revision: D5075127

fbshipit-source-id: 9e56981
---
 .../facebook/infer/annotation/Assertions.java | 53 +++++++++++++++++++
 .../java/infer/NullPointerExceptions.java     |  6 +++
 2 files changed, 59 insertions(+)
 create mode 100644 infer/models/java/src/com/facebook/infer/annotation/Assertions.java

diff --git a/infer/models/java/src/com/facebook/infer/annotation/Assertions.java b/infer/models/java/src/com/facebook/infer/annotation/Assertions.java
new file mode 100644
index 000000000..342a64ea6
--- /dev/null
+++ b/infer/models/java/src/com/facebook/infer/annotation/Assertions.java
@@ -0,0 +1,53 @@
+/*
+ * Copyright (c) 2004 - 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 com.facebook.infer.annotation;
+
+import com.facebook.infer.builtins.InferBuiltins;
+
+import javax.annotation.Nullable;
+
+public class Assertions {
+
+  public static <T> T assumeNotNull(@Nullable T object) {
+    InferBuiltins.assume_allocated(object);
+    return object;
+  }
+
+  public static <T> T assumeNotNull(@Nullable T object, String explanation) {
+    InferBuiltins.assume_allocated(object);
+    return object;
+  }
+
+  public static <T> T assertNotNull(@Nullable T object) {
+    InferBuiltins.assume_allocated(object);
+    return object;
+  }
+
+  public static <T> T assertNotNull(@Nullable T object, String explanation) {
+    InferBuiltins.assume_allocated(object);
+    return object;
+  }
+
+  public static void assumeCondition(boolean condition) {
+    InferBuiltins.assume(condition);
+  }
+
+  public static void assumeCondition(boolean condition, String explanation) {
+    InferBuiltins.assume(condition);
+  }
+
+  public static void assertCondition(boolean condition) {
+    InferBuiltins.assume(condition);
+  }
+
+  public static void assertCondition(boolean condition, String explanation) {
+    InferBuiltins.assume(condition);
+  }
+}
diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
index 47fb1727e..937952bf1 100644
--- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
+++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
@@ -16,6 +16,8 @@ import android.database.Cursor;
 import android.database.sqlite.SQLiteDatabase;
 import android.text.TextUtils;
 
+import com.facebook.infer.annotation.Assertions;
+
 import com.google.common.base.Optional;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
@@ -605,4 +607,8 @@ public class NullPointerExceptions {
     }
   }
 
+  String assertParameterNotNullableOk(@Nullable Object object) {
+    return Assertions.assertNotNull(object).toString();
+  }
+
 }