[infer][Java] rename the builtin `InferBuiltins.__infer_assume` into `InferBuiltins.assume`

master
jrm 10 years ago
parent 34b911c935
commit 2bce7c6c3d

@ -20,7 +20,8 @@ public class InferBuiltins {
public static void _exit() { 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) { public static String __split_get_nth(String s, String sep, int n) {

@ -6,10 +6,13 @@
package com.facebook.infer.models; package com.facebook.infer.models;
import com.facebook.infer.models.InferBuiltins;
import java.io.IOException; import java.io.IOException;
import java.net.SocketException; import java.net.SocketException;
import java.sql.SQLException; import java.sql.SQLException;
public class InferUndefined { public class InferUndefined {
public static native boolean boolean_undefined(); public static native boolean boolean_undefined();
@ -130,9 +133,7 @@ public class InferUndefined {
public static int nonneg_int() { public static int nonneg_int() {
int res = int_undefined(); int res = int_undefined();
if (res < 0) InferBuiltins.assume(res >= 0);
while (true) {
}
return res; return res;
} }

@ -1,12 +1,14 @@
package com.google.common.collect; package com.google.common.collect;
import com.facebook.infer.models.InferBuiltins;
public class ImmutableList<E> { public class ImmutableList<E> {
private static final ImmutableList<Object> EMPTY = new ImmutableList<Object>(); private static final ImmutableList<Object> EMPTY = new ImmutableList<Object>();
@SuppressWarnings("unchecked") @SuppressWarnings("unchecked")
public static <E> ImmutableList<E> of() { public static <E> ImmutableList<E> of() {
while (EMPTY == null) {} InferBuiltins.assume(EMPTY != null);
return (ImmutableList<E>) EMPTY; return (ImmutableList<E>) EMPTY;
} }

@ -2,6 +2,8 @@ package com.google.common.collect;
import java.util.NoSuchElementException; import java.util.NoSuchElementException;
import com.facebook.infer.models.InferBuiltins;
import javax.annotation.Nullable; import javax.annotation.Nullable;
public class Iterators { public class Iterators {
@ -33,13 +35,12 @@ public class Iterators {
@Override @Override
public T next() { public T next() {
while (value == null) {} InferBuiltins.assume(value != null);
if (done) { if (done) {
throw new NoSuchElementException(); throw new NoSuchElementException();
} }
done = true; done = true;
return value; return value;
// return null;
} }
}; };
} }

@ -9,7 +9,7 @@ public class JunitAssertion {
} }
} }
public void consistentAssumtion(A a) { public void consistentAssertion(A a) {
assertTrue(a != null); assertTrue(a != null);
a.f(); a.f();
} }

@ -35,7 +35,7 @@ public class JunitAssertionTest {
doesNotContain( doesNotContain(
NULL_DEREFERENCE, NULL_DEREFERENCE,
JunitAssertionFile, JunitAssertionFile,
"consistentAssumtion" "consistentAssertion"
) )
); );
} }

Loading…
Cancel
Save