Disable loop-less init of primitive arrays

jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.boolArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.byteArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.charArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.doubleArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.floatArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.intArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.intArrayMulti --max-nondet-array-length 51 --unwind 4
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ line 65 assertion.*: FAILURE
 --
 Check inner most array of multi-dimensional array is reachable independently of
 --unwind value.
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.longArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/NondetArrayPrimitive/shortArray.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 NondetArrayPrimitive.class
 --function NondetArrayPrimitive.shortArray --max-nondet-array-length 2000 --unwind 1
 ^VERIFICATION FAILED$
@@ -10,3 +10,4 @@ Unwinding loop __CPROVER__start.0 iteration 2
 ^warning: ignoring
 --
 Check no unwind needed to reach non-primitive array cell
+Skipped: Loop-less initialisation is disabled

jbmc/regression/jbmc/json_trace3/test.desc

@@ -4,7 +4,7 @@ Test.class
 activate-multi-line-match
 EXIT=10
 SIGNAL=0
-"lhs": "dynamic_object3\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
+"lhs": "dynamic_2_array\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
 --
 "name": "unknown"
 ^warning: ignoring

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1424,30 +1424,18 @@ void java_object_factoryt::gen_nondet_array_init(
     init_array_expr =
       typecast_exprt(init_array_expr, pointer_type(element_type));
 
-  if(element_type.id() == ID_pointer)
-  {
-    // For arrays of non-primitive types, nondeterministically initialize each
-    // element of the array
-    array_loop_init_code(
-      assignments,
-      init_array_expr,
-      length_expr,
-      element_type,
-      max_length_expr,
-      depth,
-      update_in_place,
-      location);
-  }
-  else
-  {
-    // Arrays of primitive types can be initialized with a single instruction
-    array_primitive_init_code(
-      assignments,
-      init_array_expr,
-      element_type,
-      max_length_expr,
-      location);
-  }
+  array_loop_init_code(
+    assignments,
+    init_array_expr,
+    length_expr,
+    element_type,
+    max_length_expr,
+    depth,
+    update_in_place,
+    location);
+
+  // TODO: Enable loop-less initialization of primitive arrays using
+  // array_primitive_init_code
 }
 
 /// We nondet-initialize enums to be equal to one of the constants defined