allocate_and_assign_array_from_json function

This is so that we directly declare an array of the right length instead
of giving a non-deterministic size and constraining it.

Author: romainbrenguier

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -496,6 +496,22 @@ static void assign_array_from_json(
   assign_array_data_component_from_json(expr, json, type_from_array, info);
 }
 
+/// Allocate an array of size given by the json object, and assign its elemnts
+/// according tho the json content.
+static void allocate_and_assign_array_from_json(
+  const exprt &array,
+  const jsont &json,
+  const optionalt<std::string> &type_from_array,
+  object_creation_infot &info)
+{
+  PRECONDITION(is_java_array_type(array.type()));
+  const auto &element_type =
+    java_array_element_type(to_struct_tag_type(array.type().subtype()));
+  const json_arrayt json_array = get_untyped_array(json, element_type);
+  allocate_array(array, from_integer(json_array.size(), java_int_type()), info);
+  assign_array_data_component_from_json(array, json, type_from_array, info);
+}
+
 /// One of the cases in the recursive algorithm: the case where \p expr
 /// represents a string.
 /// See \ref assign_from_json_rec.
@@ -769,10 +785,19 @@ static void assign_reference_from_json(
   {
     if(is_java_array_type(expr.type()))
     {
-      INVARIANT(
-        reference.array_length, "an array reference should stores its length");
-      assign_array_from_json(
-        reference.expr, json, *reference.array_length, type_from_array, info);
+      if(has_nondet_length(json))
+      {
+        const exprt length =
+          nondet_length(info.allocate_objects, info.block, info.loc);
+        allocate_array(expr, length, info);
+        INVARIANT(
+          reference.array_length,
+          "an array reference should stores its length");
+        assign_array_from_json(
+          reference.expr, json, *reference.array_length, type_from_array, info);
+      }
+      else
+        allocate_and_assign_array_from_json(expr, json, type_from_array, info);
     }
     else
       assign_struct_from_json(dereference_exprt(reference.expr), json, info);
@@ -811,10 +836,15 @@ void assign_from_json_rec(
     }
     else if(is_java_array_type(expr.type()))
     {
-      const exprt length =
-        nondet_length(info.allocate_objects, info.block, info.loc);
-      allocate_array(expr, length, info);
-      assign_array_from_json(expr, json, length, type_from_array, info);
+      if(has_nondet_length(json))
+      {
+        const exprt length =
+          nondet_length(info.allocate_objects, info.block, info.loc);
+        allocate_array(expr, length, info);
+        assign_array_from_json(expr, json, length, type_from_array, info);
+      }
+      else
+        allocate_and_assign_array_from_json(expr, json, type_from_array, info);
     }
     else if(
       const auto runtime_type =