Test for multi-dim array

Loop-less init: check that innermost array doesn't require unwind

Author: Joel Allred

jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class

@@ -13,4 +13,15 @@ void floatArray(float[] array)
       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.intArrayMulti --max-nondet-array-length 51 --unwind 4
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+line 23 assertion.*: FAILURE
+--
+^warning: ignoring
+--
+Check inner most array of multi-dimensional array is reachable independently of
+--unwind value.