From 78f4e8c8814f20ae04d2fb94683d1c84f8de4493 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Mon, 11 Jun 2018 16:38:45 +0100
Subject: [PATCH] Add Class literal initializer

This is used by JBMC and similar to set up Class literals (e.g. MyClass.class)
---
 src/main/java/java/lang/Class.java | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java
index d6fc803..290dcac 100644
--- a/src/main/java/java/lang/Class.java
+++ b/src/main/java/java/lang/Class.java
@@ -420,4 +420,29 @@ private static boolean desiredAssertionStatus0(Class<?> clazz) {
         // TODO does this need native handling, or is this acceptable?
         return true;
     }
+
+    // DIFFBLUE MODEL LIBRARY
+    // This method is called by CBMC to try to set class constants, which can
+    // avoid the time-consuming process of enumerating over the constant
+    // dictionary's internal array, when generating the Class object non-
+    // deterministically.
+    public void cproverInitializeClassLiteral(
+            String name,
+            boolean isAnnotation,
+            boolean isArray,
+            boolean isInterface,
+            boolean isSynthetic,
+            boolean isLocalClass,
+            boolean isMemberClass,
+            boolean isEnum) {
+        this.name = name;
+        this.isAnnotation = isAnnotation;
+        this.isArray = isArray;
+        this.isInterface = isInterface;
+        this.isSynthetic = isSynthetic;
+        this.isLocalClass = isLocalClass;
+        this.isMemberClass = isMemberClass;
+        this.isEnum = isEnum;
+    }
+
 }