From 8779b80f8a1c5195efbf547e9da496c0eb70cd81 Mon Sep 17 00:00:00 2001 From: jrm Date: Mon, 6 Jul 2015 10:48:09 -0700 Subject: [PATCH] [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. --- ...ArrayIndexOutOfBoundsExceptionExample.java | 19 +++++++++++++++++-- .../ArrayIndexOutOfBoundsExceptionTest.java | 11 ++++++++--- .../tracing/LocallyDefinedExceptionTest.java | 9 ++++++--- .../tracing/NullPointerExceptionTest.java | 9 ++++++--- .../java/tracing/ReportOnMainTest.java | 9 ++++++--- 5 files changed, 43 insertions(+), 14 deletions(-) diff --git a/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java index adffe07b2..60892d6b7 100644 --- a/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java +++ b/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java @@ -7,7 +7,9 @@ import com.facebook.infer.annotation.Verify; public class ArrayIndexOutOfBoundsExceptionExample { void callMethodFromArray(T[] array, int index) { - array[index].f(); + if (array[index] != null) { + array[index].f(); + } } @Verify @@ -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); + } + } diff --git a/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java b/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java index 941a8ad4b..7da3748a7 100644 --- a/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java +++ b/infer/tests/endtoend/java/tracing/ArrayIndexOutOfBoundsExceptionTest.java @@ -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 ) ); } diff --git a/infer/tests/endtoend/java/tracing/LocallyDefinedExceptionTest.java b/infer/tests/endtoend/java/tracing/LocallyDefinedExceptionTest.java index 4f20dd99c..bbe61a93d 100644 --- a/infer/tests/endtoend/java/tracing/LocallyDefinedExceptionTest.java +++ b/infer/tests/endtoend/java/tracing/LocallyDefinedExceptionTest.java @@ -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 ) ); } diff --git a/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java b/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java index c77d87438..a17643c31 100644 --- a/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java @@ -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 ) ); } diff --git a/infer/tests/endtoend/java/tracing/ReportOnMainTest.java b/infer/tests/endtoend/java/tracing/ReportOnMainTest.java index fd06b9dbf..0e747ef09 100644 --- a/infer/tests/endtoend/java/tracing/ReportOnMainTest.java +++ b/infer/tests/endtoend/java/tracing/ReportOnMainTest.java @@ -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 ) ); }