Update to models-library@4d20c50

Author: peterschrammel

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

@@ -39,6 +39,58 @@
 
 import org.cprover.CProver;
 
+/**
+ * Instances of the class {@code Class} represent classes and
+ * interfaces in a running Java application.  An enum is a kind of
+ * class and an annotation is a kind of interface.  Every array also
+ * belongs to a class that is reflected as a {@code Class} object
+ * that is shared by all arrays with the same element type and number
+ * of dimensions.  The primitive Java types ({@code boolean},
+ * {@code byte}, {@code char}, {@code short},
+ * {@code int}, {@code long}, {@code float}, and
+ * {@code double}), and the keyword {@code void} are also
+ * represented as {@code Class} objects.
+ *
+ * <p> {@code Class} has no public constructor. Instead {@code Class}
+ * objects are constructed automatically by the Java Virtual Machine as classes
+ * are loaded and by calls to the {@code defineClass} method in the class
+ * loader.
+ *
+ * <p> The following example uses a {@code Class} object to print the
+ * class name of an object:
+ *
+ * <blockquote><pre>
+ *     void printClassName(Object obj) {
+ *         System.out.println("The class of " + obj +
+ *                            " is " + obj.getClass().getName());
+ *     }
+ * </pre></blockquote>
+ *
+ * <p> It is also possible to get the {@code Class} object for a named
+ * type (or for void) using a class literal.  See Section 15.8.2 of
+ * <cite>The Java&trade; Language Specification</cite>.
+ * For example:
+ *
+ * <blockquote>
+ *     {@code System.out.println("The name of class Foo is: "+Foo.class.getName());}
+ * </blockquote>
+ *
+ * @param <T> the type of the class modeled by this {@code Class}
+ * object.  For example, the type of {@code String.class} is {@code
+ * Class<String>}.  Use {@code Class<?>} if the class being modeled is
+ * unknown.
+ *
+ * @author  unascribed
+ * @see     java.lang.ClassLoader#defineClass(byte[], int, int)
+ * @since   JDK1.0
+ *
+ * @diffblue.limitedSupport
+ * Generated tests that create an instance of Class will be incorrect:
+ * <ul>
+ *   <li>TG-7636: IllegalAccessError error when attempting to set the java.lang.class via reflection</li>
+ *   <li>TG-4727: When test-gen mocks java.lang.Class, it causes IllegalAccessError</li>
+ * </ul>
+ */
 public final class Class<T> {
 
     private Class() {}
@@ -453,6 +505,7 @@ private static boolean desiredAssertionStatus0(Class<?> clazz) {
     protected void cproverNondetInitialize() {
         CProver.assume(name != null);
         CProver.assume(enumConstantDirectory == null);
+        CProver.assume(classValueMap == null);
     }
 
     // DIFFBLUE MODEL LIBRARY
@@ -607,6 +660,13 @@ public Method getMethod(String name, Class<?>... parameterTypes) throws NoSuchMe
         return new Method(this, name, parameterTypes);
     }
 
+    // DIFFBLUE MODEL LIBRARY
+    // This field is never read in our model. We include them because ClassValue
+    // (in the java library, not our models) references it, so it is needed to
+    // make ClassValue compile.
+    // transient ClassValue.ClassValueMap classValueMap;
+    transient ClassValue.ClassValueMap classValueMap = null;
+
     /**
      * Returns the {@code Class} representing the component type of an
      * array.  If this class does not represent an array class this method
@@ -615,10 +675,12 @@ public Method getMethod(String name, Class<?>... parameterTypes) throws NoSuchMe
      * @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
+     * @since JDK1.1
+     * @diffblue.noSupport
      */
+    // public native Class<?> getComponentType();
     public Class<?> getComponentType() {
         CProver.notModelled();
-        return CProver.nondetWithoutNullForNotModelled();
+        return CProver.nondetWithNullForNotModelled();
     }
 }