Class: create primitive classes without calling forName

src/main/java/java/lang/Byte.java

@@ -62,8 +62,11 @@ public final class Byte extends Number implements Comparable<Byte> {
      * The {@code Class} instance representing the primitive type
      * {@code byte}.
      */
+    // DIFFBLUE MODEL LIBRARY
+    //     We use the int version of getPrimitiveClass instead of
+    //     the original String version
     @SuppressWarnings("unchecked")
-    public static final Class<Byte> TYPE = (Class<Byte>) Class.getPrimitiveClass(7);
+    public static final Class<Byte> TYPE = (Class<Byte>) Class.getPrimitiveClass(2);
 
     /**
      * Returns a new {@code String} object representing the

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

@@ -95,6 +95,14 @@ public final class Class<T> {
 
     private Class() {}
 
+    // DIFFBLUE MODEL LIBRARY Creates the Class objects of primitive types.
+    // These must not be created via forName, which is not modelled.
+    private static Class<?> cproverClassWithName(String className) {
+        Class<?> c = new Class<>();
+        c.name = className;
+        return c;
+    }
+
     private transient String name;
 
     // TODO: these boolean fields model the internal encoding of classes
@@ -391,33 +399,33 @@ private String resolveName(String name) {
 
     public Class getSuperclass(){
         // TODO: here we assume no superclass which may not be correct
-        return Class.forName(null);
+        return null;
     }
 
     public static Class getPrimitiveClass(String s){
         if("boolean".equals(s))
-            return Class.forName("boolean");
+            return cproverClassWithName("boolean");
         if("char".equals(s))
-            return Class.forName("char");
+            return cproverClassWithName("char");
         if("byte".equals(s))
-            return Class.forName("byte");
+            return cproverClassWithName("byte");
         if("short".equals(s))
-            return Class.forName("short");
+            return cproverClassWithName("short");
         if("int".equals(s))
-            return Class.forName("int");
+            return cproverClassWithName("int");
         if("long".equals(s))
-            return Class.forName("long");
+            return cproverClassWithName("long");
         if("float".equals(s))
-            return Class.forName("float");
+            return cproverClassWithName("float");
         if("double".equals(s))
-            return Class.forName("double");
+            return cproverClassWithName("double");
         if("void".equals(s))
-            return Class.forName("void");
+            return cproverClassWithName("void");
         // TODO: we should throw an exception but this does not seem to work well
         // at the moment, so we will assume it does not happen instead.
         // throw new IllegalArgumentException("Not primitive type : " + s);
         CProver.assume(false);
-        return Class.forName("");
+        return cproverClassWithName("");
     }
 
     // This version is nicer for the symbolic execution as it knows how to
@@ -428,22 +436,22 @@ public static Class getPrimitiveClass(String s){
     // takes 8 seconds while the int version takes 3 seconds.
     static Class getPrimitiveClass(int i){
         if(i==0)
-            return Class.forName("boolean");
+            return cproverClassWithName("boolean");
         if(i==1)
-            return Class.forName("char");
+            return cproverClassWithName("char");
         if(i==2)
-            return Class.forName("byte");
+            return cproverClassWithName("byte");
         if(i==3)
-            return Class.forName("short");
+            return cproverClassWithName("short");
         if(i==4)
-            return Class.forName("int");
+            return cproverClassWithName("int");
         if(i==5)
-            return Class.forName("long");
+            return cproverClassWithName("long");
         if(i==6)
-            return Class.forName("float");
+            return cproverClassWithName("float");
         if(i==7)
-            return Class.forName("double");
-        return Class.forName("void");
+            return cproverClassWithName("double");
+        return cproverClassWithName("void");
     }
 
     Map<String, T> enumConstantDirectory() {

src/main/java/java/lang/Float.java

@@ -137,8 +137,11 @@ public final class Float extends Number implements Comparable<Float> {
      *
      * @since JDK1.1
      */
+    // DIFFBLUE MODEL LIBRARY
+    //     We use the int version of getPrimitiveClass instead of
+    //     the original String version
     @SuppressWarnings("unchecked")
-    public static final Class<Float> TYPE = (Class<Float>) Class.getPrimitiveClass(7);
+    public static final Class<Float> TYPE = (Class<Float>) Class.getPrimitiveClass(6);
 
     /**
      * Returns a string representation of the {@code float}

src/main/java/java/lang/Short.java

@@ -61,8 +61,11 @@ public final class Short extends Number implements Comparable<Short> {
      * The {@code Class} instance representing the primitive type
      * {@code short}.
      */
+    // DIFFBLUE MODEL LIBRARY
+    //     We use the int version of getPrimitiveClass instead of
+    //     the original String version
     @SuppressWarnings("unchecked")
-    public static final Class<Short> TYPE = (Class<Short>) Class.getPrimitiveClass(7);
+    public static final Class<Short> TYPE = (Class<Short>) Class.getPrimitiveClass(3);
     /**
      * Returns a new {@code String} object representing the
      * specified {@code short}. The radix is assumed to be 10.