diff --git a/regression/cbmc-java/invalid_classpath/Test.class b/regression/cbmc-java/invalid_classpath/Test.class deleted file mode 100644 index aaa01c760f2..00000000000 Binary files a/regression/cbmc-java/invalid_classpath/Test.class and /dev/null differ diff --git a/regression/cbmc-java/invalid_classpath/Test.java b/regression/cbmc-java/invalid_classpath/Test.java deleted file mode 100644 index e3957a5157d..00000000000 --- a/regression/cbmc-java/invalid_classpath/Test.java +++ /dev/null @@ -1,3 +0,0 @@ -public class Test { - public void main() {} -} diff --git a/regression/cbmc-java/invalid_classpath/test-jar.desc b/regression/cbmc-java/invalid_classpath/test-jar.desc deleted file mode 100644 index ad020054856..00000000000 --- a/regression/cbmc-java/invalid_classpath/test-jar.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE symex-driven-lazy-loading-expected-failure -Test.class ---classpath ./NotHere.jar -^EXIT=6$ -^SIGNAL=0$ -^the program has no entry point$ -^failed to load class `Test'$ --- --- -symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/invalid_classpath/test-path.desc b/regression/cbmc-java/invalid_classpath/test-path.desc deleted file mode 100644 index 282ae0209f8..00000000000 --- a/regression/cbmc-java/invalid_classpath/test-path.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE symex-driven-lazy-loading-expected-failure -Test.class ---classpath ./NotHere -^EXIT=6$ -^SIGNAL=0$ -^the program has no entry point$ -^failed to load class `Test'$ --- --- -symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/provide_object_implementation/java/lang/Object.class b/regression/cbmc-java/provide_object_implementation/java/lang/Object.class deleted file mode 100644 index 868d3dbea58..00000000000 Binary files a/regression/cbmc-java/provide_object_implementation/java/lang/Object.class and /dev/null differ diff --git a/regression/cbmc-java/provide_object_implementation/java/lang/Object.java b/regression/cbmc-java/provide_object_implementation/java/lang/Object.java deleted file mode 100644 index 0ba3304a00c..00000000000 --- a/regression/cbmc-java/provide_object_implementation/java/lang/Object.java +++ /dev/null @@ -1,33 +0,0 @@ -package java.lang; - -public class Object { - public final Class getClass() { - return null; - } - - public int hashCode() { return 0; } - - public boolean equals(Object obj) { return (this == obj); } - - protected Object clone() throws CloneNotSupportedException { - throw new CloneNotSupportedException(); - } - - public String toString() { return "object"; } - - public final void notify() {} - - public final void notifyAll() {} - - public final void wait(long timeout) throws InterruptedException { - throw new InterruptedException(); - } - - public final void wait(long timeout, int nanos) throws InterruptedException { - wait(timeout); - } - - public final void wait() throws InterruptedException { wait(0); } - - protected void finalize() throws Throwable { } -} diff --git a/regression/cbmc-java/provide_object_implementation/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc deleted file mode 100644 index 381ae109d1e..00000000000 --- a/regression/cbmc-java/provide_object_implementation/test.desc +++ /dev/null @@ -1,10 +0,0 @@ -CORE symex-driven-lazy-loading-expected-failure -java/lang/Object.class - -^EXIT=6$ -^SIGNAL=0$ -^the program has no entry point$ --- -^failed to add class symbol java::java\.lang\.Object$ --- -symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index fe393c6fcf5..996d54985ba 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -185,12 +185,6 @@ 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); diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index 2196b9b7bbf..e44cf8d3052 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -81,9 +81,9 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( optionalt java_class_loadert::get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, - const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit) { + jar_indext &jar_index = jars_by_path.at(jar_file); auto jar_index_it = jar_index.find(class_name); if(jar_index_it == jar_index.end()) return {}; @@ -112,11 +112,9 @@ java_class_loadert::get_parse_tree( // First add all given JAR files for(const auto &jar_file : jar_files) { - jar_index_optcreft index = read_jar_file(class_loader_limit, jar_file); - if(!index) - continue; + read_jar_file(class_loader_limit, jar_file); optionalt parse_tree = - get_class_from_jar(class_name, jar_file, *index, class_loader_limit); + get_class_from_jar(class_name, jar_file, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } @@ -132,14 +130,12 @@ java_class_loadert::get_parse_tree( // This does not read from the jar file but from the jar_filet object we // just created - jar_index_optcreft index = read_jar_file(class_loader_limit, core_models); - if(index) - { - optionalt parse_tree = - get_class_from_jar(class_name, core_models, *index, class_loader_limit); - if(parse_tree) - parse_trees.push_back(*parse_tree); - } + read_jar_file(class_loader_limit, core_models); + + optionalt parse_tree = + get_class_from_jar(class_name, core_models, class_loader_limit); + if(parse_tree) + parse_trees.push_back(*parse_tree); } // Then add everything on the class path @@ -147,11 +143,10 @@ java_class_loadert::get_parse_tree( { if(has_suffix(cp_entry, ".jar")) { - jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry); - if(!index) - continue; + read_jar_file(class_loader_limit, cp_entry); + optionalt parse_tree = - get_class_from_jar(class_name, cp_entry, *index, class_loader_limit); + get_class_from_jar(class_name, cp_entry, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index 6f46072aaa2..cfc098e899c 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -160,7 +160,6 @@ class java_class_loadert:public messaget optionalt get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, - const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit); };