Add test (incomplete) showing clone of arrays working

Author: thk123

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

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

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

@@ -0,0 +1,6 @@
+CORE
+ArrayClone.class
+--function ArrayClone.cloneReference
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$