Skip to content

Commit 78f4e8c

Browse files
committed
Add Class literal initializer
This is used by JBMC and similar to set up Class literals (e.g. MyClass.class)
1 parent dbaaca5 commit 78f4e8c

File tree

1 file changed

+25
-0
lines changed

1 file changed

+25
-0
lines changed

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -420,4 +420,29 @@ private static boolean desiredAssertionStatus0(Class<?> clazz) {
420420
// TODO does this need native handling, or is this acceptable?
421421
return true;
422422
}
423+
424+
// DIFFBLUE MODEL LIBRARY
425+
// This method is called by CBMC to try to set class constants, which can
426+
// avoid the time-consuming process of enumerating over the constant
427+
// dictionary's internal array, when generating the Class object non-
428+
// deterministically.
429+
public void cproverInitializeClassLiteral(
430+
String name,
431+
boolean isAnnotation,
432+
boolean isArray,
433+
boolean isInterface,
434+
boolean isSynthetic,
435+
boolean isLocalClass,
436+
boolean isMemberClass,
437+
boolean isEnum) {
438+
this.name = name;
439+
this.isAnnotation = isAnnotation;
440+
this.isArray = isArray;
441+
this.isInterface = isInterface;
442+
this.isSynthetic = isSynthetic;
443+
this.isLocalClass = isLocalClass;
444+
this.isMemberClass = isMemberClass;
445+
this.isEnum = isEnum;
446+
}
447+
423448
}

0 commit comments

Comments
 (0)