Skip to content

Commit 19fa419

Browse files
Make allocate_array take location and return code
This better reflects what this function does and make it easier to refactor.
1 parent 9c0e0d3 commit 19fa419

File tree

1 file changed

+8
-7
lines changed

1 file changed

+8
-7
lines changed

jbmc/src/java_bytecode/assignments_from_json.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -422,19 +422,18 @@ static void assign_array_data_component_from_json(
422422

423423
/// Allocate a fresh array of length \p array_length_expr and assigns \p expr
424424
/// to it.
425-
static void allocate_array(
425+
static codet allocate_array(
426426
const exprt &expr,
427427
const exprt &array_length_expr,
428-
object_creation_infot &info)
428+
const source_locationt &loc)
429429
{
430430
const pointer_typet &pointer_type = to_pointer_type(expr.type());
431431
const auto &element_type =
432432
java_array_element_type(to_struct_tag_type(pointer_type.subtype()));
433433
side_effect_exprt java_new_array{ID_java_new_array, pointer_type};
434434
java_new_array.copy_to_operands(array_length_expr);
435435
java_new_array.type().subtype().set(ID_element_type, element_type);
436-
code_assignt assign{expr, java_new_array, info.loc};
437-
info.block.add(assign);
436+
return code_assignt{expr, java_new_array, loc};
438437
}
439438

440439
/// Declare a non-deterministic length expression
@@ -737,7 +736,8 @@ static std::pair<bool, object_creation_referencet> get_or_create_reference(
737736
side_effect_expr_nondett{java_int_type()}});
738737
info.block.add(code_assumet{binary_predicate_exprt{
739738
*reference.array_length, ID_ge, from_integer(0, java_int_type())}});
740-
allocate_array(reference.expr, *reference.array_length, info);
739+
info.block.add(
740+
allocate_array(reference.expr, *reference.array_length, info.loc));
741741
info.references.insert({id, reference});
742742
}
743743
else
@@ -843,7 +843,7 @@ void assign_from_json_rec(
843843
{
844844
const exprt length =
845845
nondet_length(info.allocate_objects, info.block, info.loc);
846-
allocate_array(expr, length, info);
846+
info.block.add(allocate_array(expr, length, info.loc));
847847
assign_nondet_length_array_from_json(
848848
expr, json, length, type_from_array, info);
849849
}
@@ -853,7 +853,8 @@ void assign_from_json_rec(
853853
const auto &element_type =
854854
java_array_element_type(to_struct_tag_type(expr.type().subtype()));
855855
const std::size_t length = get_untyped_array(json, element_type).size();
856-
allocate_array(expr, from_integer(length, java_int_type()), info);
856+
info.block.add(allocate_array(
857+
expr, from_integer(length, java_int_type()), info.loc));
857858
assign_array_data_component_from_json(
858859
expr, json, type_from_array, info);
859860
}

0 commit comments

Comments
 (0)