diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 9a6350a..832ad57 100644 --- a/src/main/java/java/lang/Class.java +++ b/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(); + } } diff --git a/src/main/java/org/cprover/CProver.java b/src/main/java/org/cprover/CProver.java index a1d96b0..8295a39 100644 --- a/src/main/java/org/cprover/CProver.java +++ b/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[] createArrayWithType(int length, T[] type) { + Class typeClass = type.getClass(); + return (T[])Array.newInstance(typeClass.getComponentType(), length); + } }