File tree 1 file changed +25
-0
lines changed
1 file changed +25
-0
lines changed Original file line number Diff line number Diff line change @@ -420,4 +420,29 @@ private static boolean desiredAssertionStatus0(Class<?> clazz) {
420
420
// TODO does this need native handling, or is this acceptable?
421
421
return true ;
422
422
}
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
+
423
448
}
You can’t perform that action at this time.
0 commit comments