diff --git a/regression/cbmc-java/multinewarray/multinewarray.class b/regression/cbmc-java/multinewarray/multinewarray.class index 09cb7711192..6895eaa962b 100644 Binary files a/regression/cbmc-java/multinewarray/multinewarray.class and b/regression/cbmc-java/multinewarray/multinewarray.class differ diff --git a/regression/cbmc-java/multinewarray/multinewarray.java b/regression/cbmc-java/multinewarray/multinewarray.java index ce3219586e4..62df1740671 100644 --- a/regression/cbmc-java/multinewarray/multinewarray.java +++ b/regression/cbmc-java/multinewarray/multinewarray.java @@ -12,8 +12,8 @@ public static void main(String[] args) assert some_a[0].length==3; assert some_a[0][0].length==2; - int x=10; - int y=20; + int x=3; + int y=5; int[][] int_array = new int[x][y]; for(int i=0; i(rhs.type().subtype().find("#element_type")); + assert(sub_type.id()==ID_pointer); + sub_java_new.type()=sub_type; + side_effect_exprt inc(ID_assign); inc.operands().resize(2); inc.op0()=tmp_i; @@ -866,11 +872,21 @@ void goto_convertt::do_java_new_array( dereference_exprt deref_expr( plus_exprt(data, tmp_i), data.type().subtype()); + code_blockt for_body; + symbol_exprt init_sym= + new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr(); + + code_assignt init_subarray(init_sym, sub_java_new); + code_assignt assign_subarray( + deref_expr, + typecast_exprt(init_sym, deref_expr.type())); + for_body.move_to_operands(init_subarray); + for_body.move_to_operands(assign_subarray); + for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type())); for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0()); for_loop.iter()=inc; - for_loop.body()=code_skipt(); - for_loop.body()=code_assignt(deref_expr, sub_java_new); + for_loop.body()=for_body; convert(for_loop, tmp); dest.destructive_append(tmp);