From 035ae9211b85cecdf074e3851aec1a3c27187894 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 12 Apr 2017 18:29:30 +0100 Subject: [PATCH] Restore array-set for nondet arrays This was removed because the array is certain to be overwritten with nondets, and thus the zero-init was worthless-- however, for the special case of a zero-length array the init statement was the only assignment, making the difference between the interpreter assigning it value {} and assigning it no value at all. Ideally we should omit this most of the time, but its cost is probably minimal and it's much simpler to keep it than to track down all the special cases required to deal with a symbol that is referred to but never defined in the inputs map. --- src/java_bytecode/java_object_factory.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 55dfc96931f..3846845a336 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -549,7 +549,10 @@ void java_object_factoryt::gen_nondet_array_init( side_effect_exprt java_new_array(ID_java_new_array, expr.type()); java_new_array.copy_to_operands(length_sym_expr); - java_new_array.set(ID_skip_initialize, true); + // Retain the array_set instruction for the special case of a + // zero-length array, where this will be the only assignment against + // the array's identifier. + java_new_array.set(ID_skip_initialize, false); java_new_array.type().subtype().set(ID_C_element_type, element_type); codet assign=code_assignt(expr, java_new_array); assign.add_source_location()=loc; @@ -798,4 +801,3 @@ void gen_nondet_init( typet(), update_in_place); } -