Prevent attempting to load any class twice

diffblue · Mar 28, 2018 · b882670 · b882670
1 parent 7c1dfde
commit b882670
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/regression/cbmc-java/provide_object_implementation/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 java/lang/Object.class
 
 ^EXIT=6$

diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -185,6 +185,12 @@ void java_bytecode_convert_classt::operator()(
   PRECONDITION(!parse_trees.empty());
   const irep_idt &class_name = parse_trees.front().parsed_class.name;
 
+  if (symbol_table.has_symbol("java::" + id2string(class_name)))
+  {
+    debug() << "Skip class " << class_name << " (already loaded)" << eom;
+    return;
+  }
+
   // Add array types to the symbol table
   add_array_types(symbol_table);