Merge pull request #28 from diffblue/smowton/feature/createArrayWithType

Add createArrayWithType intrinsic

Author: smowton

src/main/java/java/lang/Class.java

@@ -606,4 +606,19 @@ public Field getField(String name) throws NoSuchFieldException, SecurityExceptio
     public Method getMethod(String name, Class<?>... parameterTypes) throws NoSuchMethodException, SecurityException {
         return new Method(this, name, parameterTypes);
     }
+
+    /**
+     * Returns the {@code Class} representing the component type of an
+     * array.  If this class does not represent an array class this method
+     * returns null.
+     *
+     * @return the {@code Class} representing the component type of this
+     * class if this class is an array
+     * @see     java.lang.reflect.Array
+     * @since 1.1
+     */
+    public Class<?> getComponentType() {
+        CProver.notModelled();
+        return CProver.nondetWithoutNullForNotModelled();
+    }
 }

src/main/java/org/cprover/CProver.java

@@ -2,6 +2,7 @@
 
 import java.io.BufferedInputStream;
 import java.io.PrintStream;
+import java.lang.reflect.Array;
 
 public final class CProver
 {
@@ -350,4 +351,18 @@ public static float doubleToFloat(double d)
     CProver.assume(d == (double) converted);
     return converted;
   }
+
+  /**
+   * Instantiates (but does not populate) an array with type matching a given array,
+   * but with a potentially different length. Used by ArrayList.toArray, for example,
+   * whose internal array is an Object[] but must provide that array as a user-supplied
+   * T[], copying the runtime type of whatever array the user provided as a template.
+   *
+   * The implementation given here is correct, but JBMC cannot currently understand these
+   * reflective methods and therefore replaces this function with its own implementation.
+   */
+  public static <T> T[] createArrayWithType(int length, T[] type) {
+    Class typeClass = type.getClass();
+    return (T[])Array.newInstance(typeClass.getComponentType(), length);
+  }
 }