Move some code from assign_from_json to new file

This is in preparation for adding a new class in this file, we add there
the function and class which will be needed by this class.

Author: romainbrenguier

jbmc/src/java_bytecode/Makefile

@@ -3,6 +3,7 @@ SRC = assignments_from_json.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       ci_lazy_methods_needed.cpp \
+      code_with_references.cpp \
       convert_java_nondet.cpp \
       create_array_with_type_intrinsic.cpp \
       expr2java.cpp \

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 #include "assignments_from_json.h"
 
 #include "ci_lazy_methods_needed.h"
+#include "code_with_references.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
 #include "java_string_literals.h"
@@ -420,22 +421,6 @@ static void assign_array_data_component_from_json(
   }
 }
 
-/// Allocate a fresh array of length \p array_length_expr and assigns \p expr
-/// to it.
-static codet allocate_array(
-  const exprt &expr,
-  const exprt &array_length_expr,
-  const source_locationt &loc)
-{
-  const pointer_typet &pointer_type = to_pointer_type(expr.type());
-  const auto &element_type =
-    java_array_element_type(to_struct_tag_type(pointer_type.subtype()));
-  side_effect_exprt java_new_array{ID_java_new_array, pointer_type};
-  java_new_array.copy_to_operands(array_length_expr);
-  java_new_array.type().subtype().set(ID_element_type, element_type);
-  return code_assignt{expr, java_new_array, loc};
-}
-
 /// Declare a non-deterministic length expression
 /// \param[out] allocate: allocation functor
 /// \param[out] code: code block to which code will get appended

jbmc/src/java_bytecode/assignments_from_json.h

@@ -11,23 +11,13 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H
 #define CPROVER_JAVA_BYTECODE_ASSIGNMENTS_FROM_JSON_H
 
+#include "code_with_references.h"
 #include <util/std_code.h>
 
 class jsont;
 class symbol_table_baset;
 class ci_lazy_methods_neededt;
 
-/// Information to store when several references point to the same Java object.
-struct object_creation_referencet
-{
-  /// Expression for the symbol that stores the value that may be reference
-  /// equal to other values.
-  exprt expr;
-
-  /// If `symbol` is an array, this expression stores its length.
-  optionalt<symbol_exprt> array_length;
-};
-
 /// Given an expression \p expr representing a Java object or primitive and a
 /// JSON representation \p json of the value of a Java object or primitive of a
 /// compatible type, adds statements to \p block to assign \p expr to the

jbmc/src/java_bytecode/code_with_references.cpp

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Java bytecode
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include "code_with_references.h"
+#include "java_types.h"
+#include <util/arith_tools.h>
+
+codet allocate_array(
+  const exprt &expr,
+  const exprt &array_length_expr,
+  const source_locationt &loc)
+{
+  const pointer_typet &pointer_type = to_pointer_type(expr.type());
+  const auto &element_type =
+    java_array_element_type(to_struct_tag_type(pointer_type.subtype()));
+  side_effect_exprt java_new_array{ID_java_new_array, pointer_type};
+  java_new_array.copy_to_operands(array_length_expr);
+  java_new_array.type().subtype().set(ID_element_type, element_type);
+  return code_assignt{expr, java_new_array, loc};
+}

jbmc/src/java_bytecode/code_with_references.h

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module: Java bytecode
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
+#define CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
+
+#include <memory>
+#include <util/std_code.h>
+
+/// Allocate a fresh array of length \p array_length_expr and assigns \p expr
+/// to it.
+codet allocate_array(
+  const exprt &expr,
+  const exprt &array_length_expr,
+  const source_locationt &loc);
+
+/// Information to store when several references point to the same Java object.
+struct object_creation_referencet
+{
+  /// Expression for the symbol that stores the value that may be reference
+  /// equal to other values.
+  exprt expr;
+
+  /// If `symbol` is an array, this expression stores its length.
+  /// This should only be set once the actual elements of the array have been
+  /// seen, not the first time an `@ref` have been seen, only when `@id` is
+  /// seen.
+  optionalt<exprt> array_length;
+};
+
+#endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H