Skip to content

Commit f369b62

Browse files
Use CProver.classIdentifier in getClass model
The preprocessing of getClass will stop and we have to use CProver.classIdentifier instead.
1 parent fd0a89f commit f369b62

File tree

1 file changed

+2
-10
lines changed

1 file changed

+2
-10
lines changed

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

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,8 @@ public Object() {
4141
}
4242

4343
public final Class<?> getClass() {
44-
/*
45-
* MODELS LIBRARY {
46-
* We make this call to Class.forName to ensure it is loaded
47-
* by CBMC even with --lazy-methods on. We have to do this
48-
* because the internal support for getClass use the model of
49-
* Class.forName.
50-
* }
51-
*/
52-
Class c = Class.forName("");
53-
return CProver.nondetWithoutNullForNotModelled();
44+
// DIFFBLUE MODEL LIBRARY
45+
return Class.forName(CProver.classIdentifier(this));
5446
}
5547

5648
public int hashCode() {

0 commit comments

Comments
 (0)