diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 04f62124ba0..a01f798deed 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/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): /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index db0bca45bc3..93cfb77d5d4 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/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 diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 121f709509d..0ece655b1a7 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -26,7 +26,6 @@ Date: April 2017 #include #include "java_types.h" -#include "java_object_factory.h" #include "java_utils.h" #include "java_string_library_preprocess.h" diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp index 70d5b457f8a..3a1a7ede396 100644 --- a/src/util/allocate_objects.cpp +++ b/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); +} diff --git a/src/util/allocate_objects.h b/src/util/allocate_objects.h index 19b5522e318..40a518a88dc 100644 --- a/src/util/allocate_objects.h +++ b/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