Split assign_array_from_json into two versions

Depending on whether the array has deterministic length or not.
This will make it easier to allocate the array directly to the right
size in the deterministic case.

Author: romainbrenguier

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -468,7 +468,7 @@ static symbol_exprt nondet_length(
 /// For the assignment of the array elements, see
 /// \ref assign_array_data_component_from_json.
 /// For the overall algorithm, see \ref assign_from_json_rec.
-static void assign_array_from_json(
+static void assign_det_length_array_from_json(
   const exprt &expr,
   const jsont &json,
   const exprt &given_length_expr,
@@ -481,18 +481,30 @@ static void assign_array_from_json(
   const json_arrayt json_array = get_untyped_array(json, element_type);
   const auto number_of_elements =
     from_integer(json_array.size(), java_int_type());
-  info.block.add(code_assumet{[&]() -> exprt {
-    if(has_nondet_length(json))
-    {
-      return and_exprt{
-        binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
-        binary_predicate_exprt{
-          given_length_expr,
-          ID_le,
-          from_integer(info.max_user_array_length, java_int_type())}};
-    }
-    return equal_exprt{given_length_expr, number_of_elements};
-  }()});
+  info.block.add(
+    code_assumet{equal_exprt{given_length_expr, number_of_elements}});
+  assign_array_data_component_from_json(expr, json, type_from_array, info);
+}
+
+static void assign_nondet_length_array_from_json(
+  const exprt &expr,
+  const jsont &json,
+  const exprt &given_length_expr,
+  const optionalt<std::string> &type_from_array,
+  object_creation_infot &info)
+{
+  PRECONDITION(is_java_array_type(expr.type()));
+  const auto &element_type =
+    java_array_element_type(to_struct_tag_type(expr.type().subtype()));
+  const json_arrayt json_array = get_untyped_array(json, element_type);
+  const auto number_of_elements =
+    from_integer(json_array.size(), java_int_type());
+  info.block.add(code_assumet{and_exprt{
+    binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
+    binary_predicate_exprt{
+      given_length_expr,
+      ID_le,
+      from_integer(info.max_user_array_length, java_int_type())}}});
   assign_array_data_component_from_json(expr, json, type_from_array, info);
 }
 
@@ -771,8 +783,16 @@ static void assign_reference_from_json(
     {
       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))
+      {
+        assign_nondet_length_array_from_json(
+          reference.expr, json, *reference.array_length, type_from_array, info);
+      }
+      else
+      {
+        assign_det_length_array_from_json(
+          reference.expr, json, *reference.array_length, type_from_array, info);
+      }
     }
     else
       assign_struct_from_json(dereference_exprt(reference.expr), json, info);
@@ -814,7 +834,16 @@ void assign_from_json_rec(
       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))
+      {
+        assign_nondet_length_array_from_json(
+          expr, json, length, type_from_array, info);
+      }
+      else
+      {
+        assign_det_length_array_from_json(
+          expr, json, length, type_from_array, info);
+      }
     }
     else if(
       const auto runtime_type =