Merge pull request #638 from mgudemann/bugfix/load_java_lang_class

Daniel Kroening · web-flow · commit c1d8ff3c0eba · 2017-03-15T14:39:27.000Z
adds java.lang.Class to load queue
diff --git a/regression/cbmc-java/classtest1/classtest1.class b/regression/cbmc-java/classtest1/classtest1.class
diff --git a/regression/cbmc-java/classtest1/classtest1.java b/regression/cbmc-java/classtest1/classtest1.java
@@ -0,0 +1,11 @@
+public class classtest1
+{
+  static void main(String[] args)
+  {
+    g(classtest1.class);
+  }
+  static void g(Object c)
+  {
+    assert true;
+  }
+}
diff --git a/regression/cbmc-java/classtest1/test.desc b/regression/cbmc-java/classtest1/test.desc
@@ -0,0 +1,8 @@
+CORE
+classtest1.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp
@@ -40,6 +40,8 @@ java_bytecode_parse_treet &java_class_loadert::operator()(
   queue.push("java.lang.Object");
   // java.lang.String
   queue.push("java.lang.String");
+  // add java.lang.Class
+  queue.push("java.lang.Class");
   queue.push(class_name);
 
   while(!queue.empty())
