Skip to content

Commit 6d5a14c

Browse files
smowtontautschnig
authored andcommitted
Restore array skip-initialize flag
This allows a java-new-array instruction to indicate that the array will be completely initialized immediately afterwards, and therefore the zero-init instruction can be omitted. The nondet object factory currently uses this to note that it will non-det initialize the whole array.
1 parent 5dd3f48 commit 6d5a14c

File tree

1 file changed

+14
-11
lines changed

1 file changed

+14
-11
lines changed

src/goto-programs/builtin_functions.cpp

Lines changed: 14 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -708,17 +708,20 @@ void goto_convertt::do_java_new_array(
708708
t_p->source_location=location;
709709

710710
// zero-initialize the data
711-
exprt zero_element=
712-
zero_initializer(
713-
data.type().subtype(),
714-
location,
715-
ns,
716-
get_message_handler());
717-
codet array_set(ID_array_set);
718-
array_set.copy_to_operands(data, zero_element);
719-
goto_programt::targett t_d=dest.add_instruction(OTHER);
720-
t_d->code=array_set;
721-
t_d->source_location=location;
711+
if(!rhs.get_bool(ID_skip_initialize))
712+
{
713+
exprt zero_element=
714+
zero_initializer(
715+
data.type().subtype(),
716+
location,
717+
ns,
718+
get_message_handler());
719+
codet array_set(ID_array_set);
720+
array_set.copy_to_operands(data, zero_element);
721+
goto_programt::targett t_d=dest.add_instruction(OTHER);
722+
t_d->code=array_set;
723+
t_d->source_location=location;
724+
}
722725

723726
// multi-dimensional?
724727

0 commit comments

Comments
 (0)