Add nondet array primitive and reference tests

Author: Lukasz A.J. Wrona

jbmc/regression/jbmc/lambda1/Nondet.class

@@ -5,4 +5,12 @@ public static void test(Nondet nondet) {
     Function<Integer, Integer> lambda = (z) -> nondet.x + nondet.y + z;
     assert(lambda.apply(0) == 42);
   }
+  public static void testPrimitiveArray(int[] ints) {
+    Function<Integer, Integer> lambda = (index) -> ints[index];
+    assert(lambda.apply(0) == 42);
+  }
+  public static void testReferenceArray(Nondet[] nondets) {
+    Function<Integer, Integer> lambda = (index) -> nondets[index].x;
+    assert(lambda.apply(0) == 42);
+  }
 }

jbmc/regression/jbmc/lambda1/Nondet.java

@@ -0,0 +1,10 @@
+CORE
+Nondet.class
+--function Nondet.testPrimitiveArray --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+line 10 assertion.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that primitive arrays created by the object factory can be
+captured by a lambda

jbmc/regression/jbmc/lambda1/primitive_array.desc

@@ -0,0 +1,10 @@
+CORE
+Nondet.class
+--function Nondet.testReferenceArray --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+line 14 assertion.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that reference arrays created by the object factory can be
+captured by a lambda