Move make_allocate_code to java_object_factory

Will also be used in java_object_factory

Author: Joel Allred

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1198,6 +1198,18 @@ void java_object_factoryt::allocate_nondet_length_array(
   assignments.add(assign);
 }
 
+/// Create code allocating object of size `size` and assigning it to `lhs`
+/// \param lhs : pointer which will be allocated
+/// \param size : size of the object
+/// \return code allocation object and assigning `lhs`
+codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
+{
+  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
+  alloc.add_to_operands(size);
+  alloc.add_to_operands(false_exprt());
+  return code_assignt(lhs, alloc);
+}
+
 /// Create code to initialize a Java array whose size will be at most
 /// `max_nondet_array_length`. The code is emitted to \p assignments does as
 /// follows:

jbmc/src/java_bytecode/java_object_factory.h

@@ -126,4 +126,6 @@ void gen_nondet_init(
   const java_object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place);
 
+codet make_allocate_code(const symbol_exprt &lhs, const exprt &size);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -627,18 +627,6 @@ codet java_string_library_preprocesst::code_return_function_application(
   return code_returnt(fun_app);
 }
 
-/// Create code allocating object of size `size` and assigning it to `lhs`
-/// \param lhs : pointer which will be allocated
-/// \param size : size of the object
-/// \return code allocation object and assigning `lhs`
-static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
-{
-  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
-  alloc.add_to_operands(size);
-  alloc.add_to_operands(false_exprt());
-  return code_assignt(lhs, alloc);
-}
-
 /// Declare a fresh symbol of type array of character with infinite size.
 /// \param symbol_table: the symbol table
 /// \param loc: source location