Skip to content

Commit 2eb3545

Browse files
smowtonpeterschrammel
authored andcommitted
Add Class literal initializer
This is used by JBMC and similar to set up Class literals (e.g. MyClass.class)
1 parent cf3393d commit 2eb3545

File tree

1 file changed

+24
-0
lines changed

1 file changed

+24
-0
lines changed

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

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -444,4 +444,28 @@ protected void cproverNondetInitialize() {
444444
CProver.assume(enumConstantDirectory == null);
445445
}
446446

447+
// DIFFBLUE MODEL LIBRARY
448+
// This method is called by CBMC to try to set class constants, which can
449+
// avoid the time-consuming process of enumerating over the constant
450+
// dictionary's internal array, when generating the Class object non-
451+
// deterministically.
452+
public void cproverInitializeClassLiteral(
453+
String name,
454+
boolean isAnnotation,
455+
boolean isArray,
456+
boolean isInterface,
457+
boolean isSynthetic,
458+
boolean isLocalClass,
459+
boolean isMemberClass,
460+
boolean isEnum) {
461+
this.name = name;
462+
this.isAnnotation = isAnnotation;
463+
this.isArray = isArray;
464+
this.isInterface = isInterface;
465+
this.isSynthetic = isSynthetic;
466+
this.isLocalClass = isLocalClass;
467+
this.isMemberClass = isMemberClass;
468+
this.isEnum = isEnum;
469+
}
470+
447471
}

0 commit comments

Comments
 (0)