From 4473f0692f89d28fc2def116aed180c0006efbac Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 23 Mar 2017 12:36:17 +0000
Subject: [PATCH 1/2] Fix Java multinewarray

Simply assigning to a temporary symbol of the correct type and
amending the type passed to the elaboration of the sub-array seems
to suffice to properly initialise a multi-dimensional array.
---
 src/goto-programs/builtin_functions.cpp | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 615470b7f9e..1f9e790b9d9 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -851,13 +851,19 @@ void goto_convertt::do_java_new_array(
     goto_programt tmp;
 
     symbol_exprt tmp_i=
-      new_tmp_symbol(index_type(), "index", tmp, location).symbol_expr();
+      new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
 
     code_fort for_loop;
 
     side_effect_exprt sub_java_new=rhs;
     sub_java_new.operands().erase(sub_java_new.operands().begin());
 
+    assert(rhs.type().id()==ID_pointer);
+    typet sub_type=
+      static_cast<const typet &>(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);

From 0a53fbbb74ce7dfbb8177e159dc7520906fcba0b Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 23 Mar 2017 12:41:35 +0000
Subject: [PATCH 2/2] Amend test-case to complete in acceptable time

---
 .../cbmc-java/multinewarray/multinewarray.class | Bin 773 -> 771 bytes
 .../cbmc-java/multinewarray/multinewarray.java  |   4 ++--
 regression/cbmc-java/multinewarray/test.desc    |   2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc-java/multinewarray/multinewarray.class b/regression/cbmc-java/multinewarray/multinewarray.class
index 09cb7711192f8203faf62662cb4b7ed4025996ce..6895eaa962b3d52d89596646be14ff9b8bebc37e 100644
GIT binary patch
delta 84
zcmZo=Yi8T9pON!B0}BH?0|P_T<P(fu%xtzClf{|BjC>db82lIn8NwKZ8R8j47%~_{
k8A^e4HIU!PAjKdA)S=G6{)a(^oq<VI{67QV<oQf#0JMM)Gynhq

delta 86
zcmZo>Yh~N8pONz?0}BH?0|P_L<P(futO8uN0wR+|nZk^G83Y&t7z7z27=#%T8AKSe
m7(^M$fpjg9-^?JzAOzH-&cObML57`yNmTqlgTUmuOlbhmRS$On

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<x; ++i)
diff --git a/regression/cbmc-java/multinewarray/test.desc b/regression/cbmc-java/multinewarray/test.desc
index 03395e9beaa..29e1c885a92 100644
--- a/regression/cbmc-java/multinewarray/test.desc
+++ b/regression/cbmc-java/multinewarray/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 multinewarray.class
 
 ^EXIT=0$