diff --git a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java index 996901f52..be26d6445 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java @@ -20,7 +20,8 @@ public class InferBuiltins { public static void _exit() { } - public static void __infer_assume(boolean condition) { + public static void assume(boolean condition) { + while (!condition) {} } public static String __split_get_nth(String s, String sep, int n) { diff --git a/infer/models/java/src/com/facebook/infer/models/InferUndefined.java b/infer/models/java/src/com/facebook/infer/models/InferUndefined.java index a8e7a672a..418de00b8 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferUndefined.java +++ b/infer/models/java/src/com/facebook/infer/models/InferUndefined.java @@ -6,10 +6,13 @@ package com.facebook.infer.models; +import com.facebook.infer.models.InferBuiltins; + import java.io.IOException; import java.net.SocketException; import java.sql.SQLException; + public class InferUndefined { public static native boolean boolean_undefined(); @@ -130,9 +133,7 @@ public class InferUndefined { public static int nonneg_int() { int res = int_undefined(); - if (res < 0) - while (true) { - } + InferBuiltins.assume(res >= 0); return res; } diff --git a/infer/models/java/src/com/google/common/collect/ImmutableList.java b/infer/models/java/src/com/google/common/collect/ImmutableList.java index 289bb69ec..17671656b 100644 --- a/infer/models/java/src/com/google/common/collect/ImmutableList.java +++ b/infer/models/java/src/com/google/common/collect/ImmutableList.java @@ -1,12 +1,14 @@ package com.google.common.collect; +import com.facebook.infer.models.InferBuiltins; + public class ImmutableList { private static final ImmutableList EMPTY = new ImmutableList(); @SuppressWarnings("unchecked") public static ImmutableList of() { - while (EMPTY == null) {} + InferBuiltins.assume(EMPTY != null); return (ImmutableList) EMPTY; } diff --git a/infer/models/java/src/com/google/common/collect/Iterators.java b/infer/models/java/src/com/google/common/collect/Iterators.java index 6a57778de..6a6e8c6b6 100644 --- a/infer/models/java/src/com/google/common/collect/Iterators.java +++ b/infer/models/java/src/com/google/common/collect/Iterators.java @@ -2,6 +2,8 @@ package com.google.common.collect; import java.util.NoSuchElementException; +import com.facebook.infer.models.InferBuiltins; + import javax.annotation.Nullable; public class Iterators { @@ -33,13 +35,12 @@ public class Iterators { @Override public T next() { - while (value == null) {} + InferBuiltins.assume(value != null); if (done) { throw new NoSuchElementException(); } done = true; return value; -// return null; } }; } diff --git a/infer/tests/codetoanalyze/java/infer/JunitAssertion.java b/infer/tests/codetoanalyze/java/infer/JunitAssertion.java index 0a66de798..757ed8642 100644 --- a/infer/tests/codetoanalyze/java/infer/JunitAssertion.java +++ b/infer/tests/codetoanalyze/java/infer/JunitAssertion.java @@ -9,7 +9,7 @@ public class JunitAssertion { } } - public void consistentAssumtion(A a) { + public void consistentAssertion(A a) { assertTrue(a != null); a.f(); } diff --git a/infer/tests/endtoend/java/infer/JunitAssertionTest.java b/infer/tests/endtoend/java/infer/JunitAssertionTest.java index 9817ad926..0b008994f 100644 --- a/infer/tests/endtoend/java/infer/JunitAssertionTest.java +++ b/infer/tests/endtoend/java/infer/JunitAssertionTest.java @@ -35,7 +35,7 @@ public class JunitAssertionTest { doesNotContain( NULL_DEREFERENCE, JunitAssertionFile, - "consistentAssumtion" + "consistentAssertion" ) ); }