Tests for loop-less array init

Author: Joel Allred

jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class

@@ -0,0 +1,69 @@
+class NondetArrayPrimitive
+{
+  void intArray(int[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 42) {
+      assert false;
+    }
+  }
+
+  void floatArray(float[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 42.0) {
+      assert false;
+    }
+  }
+
+  void charArray(char[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 'f') {
+      assert false;
+    }
+  }
+
+  void doubleArray(double[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 42.0) {
+      assert false;
+    }
+  }
+
+  void longArray(long[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 42) {
+      assert false;
+    }
+  }
+
+  void shortArray(short[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 42) {
+      assert false;
+    }
+  }
+
+  void byteArray(byte[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == 42) {
+      assert false;
+    }
+  }
+
+  void boolArray(boolean[] array)
+  {
+    if (array != null && array.length > 1500 && array[1500] == true) {
+      assert false;
+    }
+  }
+
+  void intArrayMulti(int[][] array)
+  {
+    if (array != null &&
+        array.length > 2 &&
+        array[2].length > 50 &&
+        array[2][50] == 42) {
+      assert false;
+    }
+  }
+
+}

jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.boolArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 55 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.byteArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 48 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.charArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 20 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.doubleArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 27 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.floatArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 13 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.intArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 6 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.intArrayMulti --max-nondet-array-length 51 --unwind 4
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 65 assertion.*: FAILURE
+--
+^warning: ignoring
+--
+Check inner most array of multi-dimensional array is reachable independently of
+--unwind value.

jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.longArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 34 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell

jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc

@@ -0,0 +1,12 @@
+CORE
+NondetArrayPrimitive.class
+--function NondetArrayPrimitive.shortArray --max-nondet-array-length 2000 --unwind 1
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 41 assertion.*: FAILURE
+--
+Unwinding loop __CPROVER__start.0 iteration 2
+^warning: ignoring
+--
+Check no unwind needed to reach non-primitive array cell