Clone reference array

jbmc/regression/jbmc/array-clone/ArrayClone.java

@@ -0,0 +1,92 @@
+public class ArrayClone {
+  public static void cloneReferenceArray() {
+    ArrayClone[] a = {new ArrayClone(), new ArrayClone() };
+    ArrayClone[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneObjectArray() {
+    Object[] a = {new Object(), new Object() };
+    Object[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneByteArray() {
+    byte[] a = {(byte) 1, (byte) 2};
+    byte[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneShortArray() {
+    short[] a = {(short) 1, (short) 2};
+    short[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneIntArray() {
+    int[] a = {1, 2};
+    int[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneLongArray() {
+    long[] a = {1L, 2L };
+    long[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+    public static void cloneFloatArray() {
+    float[] a = {1.0f, 2.0f};
+    float[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneDoubleArray() {
+    double[] a = {1.0, 2.0};
+    double[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+  public static void cloneBooleanArray() {
+    boolean[] a = {true, false};
+    boolean[] clone = a.clone();
+
+    assert(a.length == clone.length);
+    assert(a[0] == clone[0]);
+    assert(a[1] == clone[1]);
+    assert(a != clone);
+  }
+
+}

jbmc/regression/jbmc/array-clone/testBoolean.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneBooleanArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that the clone works on a boolean array

jbmc/regression/jbmc/array-clone/testByte.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneByteArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for byte arrays

jbmc/regression/jbmc/array-clone/testDouble.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneDoubleArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for double arrays

jbmc/regression/jbmc/array-clone/testFloat.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneFloatArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for float arrays

jbmc/regression/jbmc/array-clone/testInt.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneIntArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for int arrays

jbmc/regression/jbmc/array-clone/testLong.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneLongArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for long arrays

jbmc/regression/jbmc/array-clone/testObject.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneObjectArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for arrays of objects

jbmc/regression/jbmc/array-clone/testReference.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneReferenceArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for reference (non-object) arrays

jbmc/regression/jbmc/array-clone/testShort.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneShortArray
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that clone works correctly for short arrays

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -138,7 +138,9 @@ void ci_lazy_methods_neededt::gather_field_types(
     {
       const typet &element_type =
         java_array_element_type(to_struct_tag_type(class_type));
-      if(element_type.id() == ID_pointer)
+      if(
+        element_type.id() == ID_pointer &&
+        element_type.subtype().id() != ID_empty)
       {
         // This is a reference array -- mark its element type available.
         add_all_needed_classes(to_pointer_type(element_type));