[infer][tracing] add an example of inter-procedural array out of bounds error

Summary:
In tracing mode, Infer can compute pre-condtions for hitting a array access out of bounds. Adding a small such example in the tests.
master
jrm 10 years ago
parent 9e3e250fb9
commit 8779b80f8a

@ -7,8 +7,10 @@ import com.facebook.infer.annotation.Verify;
public class ArrayIndexOutOfBoundsExceptionExample {
void callMethodFromArray(T[] array, int index) {
if (array[index] != null) {
array[index].f();
}
}
@Verify
void callWithWrongIndex(T[] array, int index) {
@ -19,10 +21,23 @@ public class ArrayIndexOutOfBoundsExceptionExample {
}
}
@Verify
void callOutOfBound() {
T[] array = new T[42];
callMethodFromArray(array, -5);
}
void callAtIndex(T[] array, int index) {
array[index].f();
}
void withFixedIndex(T[] array) {
int index = 9;
callAtIndex(array, index);
}
void ArrayIndexOutOfBoundsInCallee() {
T[] array = new T[8];
withFixedIndex(array);
}
}

@ -3,7 +3,7 @@
package endtoend.java.tracing;
import static org.hamcrest.MatcherAssert.assertThat;
import static utils.matchers.ResultContainsErrorInMethod.contains;
import static utils.matchers.ResultContainsExactly.containsExactly;
import org.junit.BeforeClass;
import org.junit.Test;
@ -33,13 +33,18 @@ public class ArrayIndexOutOfBoundsExceptionTest {
@Test
public void whenEradicateRunsOnConstructorThenFieldNotInitializedIsFound()
throws IOException, InterruptedException, InferException {
String[] methods = {
"callOutOfBound",
"callWithWrongIndex",
"ArrayIndexOutOfBoundsInCallee",
};
assertThat(
"Results should contain " + ARRAY_OUT_OF_BOUND,
inferResults,
contains(
containsExactly(
ARRAY_OUT_OF_BOUND,
SOURCE_FILE,
"callOutOfBound"
methods
)
);
}

@ -1,7 +1,7 @@
package endtoend.java.tracing;
import static org.hamcrest.MatcherAssert.assertThat;
import static utils.matchers.ResultContainsErrorInMethod.contains;
import static utils.matchers.ResultContainsExactly.containsExactly;
import org.junit.BeforeClass;
import org.junit.Test;
@ -31,13 +31,16 @@ public class LocallyDefinedExceptionTest {
@Test
public void whenEradicateRunsOnConstructorThenFieldNotInitializedIsFound()
throws IOException, InterruptedException, InferException {
String[] methods = {
"fieldInvariant"
};
assertThat(
"Results should contain " + LOCALLY_DEFINED_EXCEPTION,
inferResults,
contains(
containsExactly(
LOCALLY_DEFINED_EXCEPTION,
SOURCE_FILE,
"fieldInvariant"
methods
)
);
}

@ -3,7 +3,7 @@
package endtoend.java.tracing;
import static org.hamcrest.MatcherAssert.assertThat;
import static utils.matchers.ResultContainsErrorInMethod.contains;
import static utils.matchers.ResultContainsExactly.containsExactly;
import org.junit.BeforeClass;
import org.junit.Test;
@ -33,13 +33,16 @@ public class NullPointerExceptionTest {
@Test
public void whenEradicateRunsOnConstructorThenFieldNotInitializedIsFound()
throws IOException, InterruptedException, InferException {
String[] methods = {
"callDeref"
};
assertThat(
"Results should contain " + NPE,
inferResults,
contains(
containsExactly(
NPE,
SOURCE_FILE,
"callDeref"
methods
)
);
}

@ -3,7 +3,7 @@
package endtoend.java.tracing;
import static org.hamcrest.MatcherAssert.assertThat;
import static utils.matchers.ResultContainsErrorInMethod.contains;
import static utils.matchers.ResultContainsExactly.containsExactly;
import org.junit.BeforeClass;
import org.junit.Test;
@ -33,13 +33,16 @@ public class ReportOnMainTest {
@Test
public void whenEradicateRunsOnConstructorThenFieldNotInitializedIsFound()
throws IOException, InterruptedException, InferException {
String[] methods = {
"main"
};
assertThat(
"Results should contain " + NPE,
inferResults,
contains(
containsExactly(
NPE,
SOURCE_FILE,
"main"
methods
)
);
}

Loading…
Cancel
Save