Merge pull request #4408 from smowton/smowton/fix/multianewarray-line-numbers

multianewarray instruction: don't require a source line number

Author: smowton

jbmc/regression/jbmc/multinewarray/A.class

@@ -0,0 +1 @@
+class A { }

jbmc/regression/jbmc/multinewarray/A.java

@@ -1,7 +1,3 @@
-class A
-{
-}
-
 class multinewarray
 {
   public static void main(String[] args)

jbmc/regression/jbmc/multinewarray/multinewarray.class

@@ -0,0 +1,23 @@
+class multinewarrayNoDebug
+{
+  public static void main(String[] args)
+  {
+    int[][][] some_a = new int[4][3][2];
+
+    assert some_a.length==4;
+    assert some_a[0].length==3;
+    assert some_a[0][0].length==2;
+
+    int x=3;
+    int y=5;
+    int[][] int_array = new int[x][y];
+
+    for(int i=0; i<x; ++i)
+      for(int j=0; j<x; ++j)
+        int_array[i][j]=i+j;
+
+    assert int_array[2][1] == 3;
+    A object_array[][] = new A[x][y];
+  }
+}
+

jbmc/regression/jbmc/multinewarray/multinewarray.java

@@ -0,0 +1,10 @@
+CORE
+multinewarrayNoDebug.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+If recompiling the class file, use `-g:none` to eliminate all debug info, including line number tables.

jbmc/regression/jbmc/multinewarray/multinewarrayNoDebug.class

@@ -2430,7 +2430,6 @@ code_blockt java_bytecode_convert_methodt::convert_multianewarray(
   const exprt::operandst &op,
   exprt::operandst &results)
 {
-  PRECONDITION(!location.get_line().empty());
   const reference_typet ref_type = java_reference_type(arg0.type());
   side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.operands() = op;