From fd0a89ff2cab1f7fbc52db5b12a73b34244a0b36 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 11 Apr 2019 09:02:35 +0100 Subject: [PATCH 1/2] Add String CProver.classIdentifier(Object) method This is meant to be replaced by java bytecode preprocessing of JBMC and to be used by models such as Object.getClass. --- src/main/java/org/cprover/CProver.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/main/java/org/cprover/CProver.java b/src/main/java/org/cprover/CProver.java index b94bcb9..1508f0f 100644 --- a/src/main/java/org/cprover/CProver.java +++ b/src/main/java/org/cprover/CProver.java @@ -314,4 +314,12 @@ public static int getMonitorCount(Object object) { return object.cproverMonitorCount; } + + /** + * Class identifier of an Object. For instance "java.lang.String", "java.lang.Interger". + */ + public static String classIdentifier(Object object) + { + return object.getClass().getCanonicalName(); + } } From f369b62eeddc30581b9ab6ab51d195748be15fd5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 11 Apr 2019 09:04:12 +0100 Subject: [PATCH 2/2] Use CProver.classIdentifier in getClass model The preprocessing of getClass will stop and we have to use CProver.classIdentifier instead. --- src/main/java/java/lang/Object.java | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/main/java/java/lang/Object.java b/src/main/java/java/lang/Object.java index a9e3b2e..ba9bf63 100644 --- a/src/main/java/java/lang/Object.java +++ b/src/main/java/java/lang/Object.java @@ -41,16 +41,8 @@ public Object() { } public final Class getClass() { - /* - * MODELS LIBRARY { - * We make this call to Class.forName to ensure it is loaded - * by CBMC even with --lazy-methods on. We have to do this - * because the internal support for getClass use the model of - * Class.forName. - * } - */ - Class c = Class.forName(""); - return CProver.nondetWithoutNullForNotModelled(); + // DIFFBLUE MODEL LIBRARY + return Class.forName(CProver.classIdentifier(this)); } public int hashCode() {