Skip to content

Commit 4615184

Browse files
committed
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 531ef7e commit 4615184

File tree

1 file changed

+14
-11
lines changed

1 file changed

+14
-11
lines changed

src/goto-programs/builtin_functions.cpp

+14-11
Original file line numberDiff line numberDiff line change
@@ -837,17 +837,20 @@ void goto_convertt::do_java_new_array(
837837
t_p->source_location=location;
838838

839839
// zero-initialize the data
840-
exprt zero_element=
841-
zero_initializer(
842-
data.type().subtype(),
843-
location,
844-
ns,
845-
get_message_handler());
846-
codet array_set(ID_array_set);
847-
array_set.copy_to_operands(data, zero_element);
848-
goto_programt::targett t_d=dest.add_instruction(OTHER);
849-
t_d->code=array_set;
850-
t_d->source_location=location;
840+
if(!rhs.get_bool(ID_skip_initialize))
841+
{
842+
exprt zero_element=
843+
zero_initializer(
844+
data.type().subtype(),
845+
location,
846+
ns,
847+
get_message_handler());
848+
codet array_set(ID_array_set);
849+
array_set.copy_to_operands(data, zero_element);
850+
goto_programt::targett t_d=dest.add_instruction(OTHER);
851+
t_d->code=array_set;
852+
t_d->source_location=location;
853+
}
851854

852855
// multi-dimensional?
853856

0 commit comments

Comments
 (0)