From 46151843eb88fba6ef5243da2d23441ff510bdae Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 10 Apr 2017 10:48:47 +0100 Subject: [PATCH] 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. --- src/goto-programs/builtin_functions.cpp | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 359c25dc270..d5e27615d3d 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -837,17 +837,20 @@ void goto_convertt::do_java_new_array( t_p->source_location=location; // zero-initialize the data - exprt zero_element= - zero_initializer( - data.type().subtype(), - location, - ns, - get_message_handler()); - codet array_set(ID_array_set); - array_set.copy_to_operands(data, zero_element); - goto_programt::targett t_d=dest.add_instruction(OTHER); - t_d->code=array_set; - t_d->source_location=location; + if(!rhs.get_bool(ID_skip_initialize)) + { + exprt zero_element= + zero_initializer( + data.type().subtype(), + location, + ns, + get_message_handler()); + codet array_set(ID_array_set); + array_set.copy_to_operands(data, zero_element); + goto_programt::targett t_d=dest.add_instruction(OTHER); + t_d->code=array_set; + t_d->source_location=location; + } // multi-dimensional?