CProver.classIdentifier declaration and model for Object.getClass

src/main/java/java/lang/Object.java

@@ -41,16 +41,8 @@ public Object() {
     }
 
     public final Class<?> getClass() {
-      /*
-       * MODELS LIBRARY {
-       *   We make this call to Class.forName to ensure it is loaded
-       *   by CBMC even with --lazy-methods on. We have to do this
-       *   because the internal support for getClass use the model of
-       *   Class.forName.
-       * }
-       */
-      Class c = Class.forName("");
-      return CProver.nondetWithoutNullForNotModelled();
+      // DIFFBLUE MODEL LIBRARY
+      return Class.forName(CProver.classIdentifier(this));
     }
 
     public int hashCode() {

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

@@ -314,4 +314,12 @@ public static int getMonitorCount(Object object)
   {
     return object.cproverMonitorCount;
   }
+
+  /**
+   * Class identifier of an Object. For instance "java.lang.String", "java.lang.Interger".
+   */
+  public static String classIdentifier(Object object)
+  {
+    return object.getClass().getCanonicalName();
+  }
 }