Test for loop-less array init

Author: Joel Allred

jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class

@@ -0,0 +1,16 @@
+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;
+    }
+  }
+}

jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java

@@ -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