Merge pull request #4349 from antlechner/antonia/move_make_allocate_code

Move make_allocate_code utility function

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1194,18 +1194,6 @@ 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 nondeterministically initialize arrays of primitive type.
 /// The code produced is of the form (for an array of type TYPE):
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

jbmc/src/java_bytecode/java_object_factory.h

@@ -126,6 +126,4 @@ 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

@@ -26,7 +26,6 @@ Date:   April 2017
 #include <util/string_expr.h>
 
 #include "java_types.h"
-#include "java_object_factory.h"
 #include "java_utils.h"
 
 #include "java_string_library_preprocess.h"

src/util/allocate_objects.cpp

@@ -159,12 +159,6 @@ exprt allocate_objectst::allocate_dynamic_object(
   auto object_size = size_of_expr(allocate_type, ns);
   INVARIANT(object_size.has_value(), "Size of objects should be known");
 
-  // malloc expression
-  side_effect_exprt malloc_expr(
-    ID_allocate, pointer_type(allocate_type), source_location);
-  malloc_expr.copy_to_operands(object_size.value());
-  malloc_expr.copy_to_operands(false_exprt());
-
   // create a symbol for the malloc expression so we can initialize
   // without having to do it potentially through a double-deref, which
   // breaks the to-SSA phase.
@@ -178,8 +172,8 @@ exprt allocate_objectst::allocate_dynamic_object(
 
   symbols_created.push_back(&malloc_sym);
 
-  code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
-  assign.add_source_location() = source_location;
+  code_assignt assign =
+    make_allocate_code(malloc_sym.symbol_expr(), object_size.value());
   output_code.add(assign);
 
   exprt malloc_symbol_expr = typecast_exprt::conditional_cast(
@@ -271,3 +265,10 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code)
     init_code.add(std::move(input_code));
   }
 }
+
+code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
+{
+  side_effect_exprt alloc{
+    ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
+  return code_assignt(lhs, alloc);
+}

src/util/allocate_objects.h

@@ -95,4 +95,10 @@ class allocate_objectst
     const irep_idt &basename_prefix);
 };
 
+/// Create code allocating an object of size `size` and assigning it to `lhs`
+/// \param lhs: pointer which will be allocated
+/// \param size: size of the object
+/// \return code allocating the object and assigning it to `lhs`
+code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size);
+
 #endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H