diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 8499e5913e6..e72ad355529 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -213,8 +213,7 @@ bool java_bytecode_languaget::parse( java_cp_include_files); if(config.java.main_class.empty()) { - auto manifest= - java_class_loader.jar_pool(class_loader_limit, path).get_manifest(); + auto manifest = java_class_loader.jar_pool(path).get_manifest(); std::string manifest_main_class=manifest["Main-Class"]; // if the manifest declares a Main-Class line, we got a main class @@ -228,7 +227,7 @@ bool java_bytecode_languaget::parse( if(main_class.empty()) { status() << "JAR file without entry point: loading class files" << eom; - java_class_loader.load_entire_jar(class_loader_limit, path); + java_class_loader.load_entire_jar(path); for(const auto &kv : java_class_loader.get_jar_index(path)) main_jar_classes.push_back(kv.first); } diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index b6a98f2160e..215e6739f9b 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -72,8 +72,7 @@ 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) + const jar_indext &jar_index) { auto jar_index_it = jar_index.find(class_name); if(jar_index_it == jar_index.end()) @@ -82,8 +81,7 @@ optionalt java_class_loadert::get_class_from_jar( debug() << "Getting class `" << class_name << "' from JAR " << jar_file << eom; - auto data = - jar_pool(class_loader_limit, jar_file).get_entry(jar_index_it->second); + auto data = jar_pool(jar_file).get_entry(jar_index_it->second); if(!data.has_value()) return {}; @@ -129,11 +127,11 @@ 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); + jar_index_optcreft index = read_jar_file(jar_file); if(!index) continue; optionalt parse_tree = - get_class_from_jar(class_name, jar_file, *index, class_loader_limit); + get_class_from_jar(class_name, jar_file, *index); if(parse_tree) parse_trees.emplace_back(std::move(*parse_tree)); } @@ -143,11 +141,11 @@ java_class_loadert::get_parse_tree( { if(has_suffix(cp_entry, ".jar")) { - jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry); + jar_index_optcreft index = read_jar_file(cp_entry); if(!index) continue; optionalt parse_tree = - get_class_from_jar(class_name, cp_entry, *index, class_loader_limit); + get_class_from_jar(class_name, cp_entry, *index); if(parse_tree) parse_trees.emplace_back(std::move(*parse_tree)); } @@ -230,10 +228,9 @@ java_class_loadert::get_parse_tree( } void java_class_loadert::load_entire_jar( - java_class_loader_limitt &class_loader_limit, const std::string &jar_path) { - jar_index_optcreft jar_index = read_jar_file(class_loader_limit, jar_path); + jar_index_optcreft jar_index = read_jar_file(jar_path); if(!jar_index) return; @@ -246,7 +243,6 @@ void java_class_loadert::load_entire_jar( } java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( - java_class_loader_limitt &class_loader_limit, const std::string &jar_path) { auto existing_it = jars_by_path.find(jar_path); @@ -256,7 +252,7 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( std::vector filenames; try { - filenames = this->jar_pool(class_loader_limit, jar_path).filenames(); + filenames = this->jar_pool(jar_path).filenames(); } catch(const std::runtime_error &) { @@ -266,7 +262,7 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( debug() << "Adding JAR file `" << jar_path << "'" << eom; // Create a new entry in the map and initialize using the list of file names - // that were retained in the jar_filet by the class_loader_limit filter + // that are in jar_filet jar_indext &jar_index = jars_by_path[jar_path]; for(auto &file_name : filenames) { @@ -331,7 +327,6 @@ std::string java_class_loadert::class_name_to_file(const irep_idt &class_name) } jar_filet &java_class_loadert::jar_pool( - java_class_loader_limitt &class_loader_limit, const std::string &file_name) { const auto it=m_archives.find(file_name); @@ -346,7 +341,6 @@ jar_filet &java_class_loadert::jar_pool( } jar_filet &java_class_loadert::jar_pool( - java_class_loader_limitt &class_loader_limit, const std::string &buffer_name, const void *pmem, size_t size) diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index 2f9634bb182..ed389a4d03b 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -81,7 +81,7 @@ class java_class_loadert:public messaget static std::string file_to_class_name(const std::string &); static std::string class_name_to_file(const irep_idt &); - void load_entire_jar(java_class_loader_limitt &, const std::string &jar_path); + void load_entire_jar(const std::string &jar_path); const jar_indext &get_jar_index(const std::string &jar_path) { @@ -100,20 +100,16 @@ class java_class_loadert:public messaget } /// Load jar archive or retrieve from cache if already loaded - /// \param limit /// \param filename name of the file - jar_filet &jar_pool( - java_class_loader_limitt &limit, const std::string &filename); + jar_filet &jar_pool(const std::string &filename); /// Load jar archive or retrieve from cache if already loaded - /// \param limit /// \param buffer_name name of the original file /// \param pmem memory pointer to the contents of the file /// \param size size of the memory buffer /// Note that this mocks the existence of a file which may /// or may not exist since the actual data bis retrieved from memory. jar_filet &jar_pool( - java_class_loader_limitt &limit, const std::string &buffer_name, const void *pmem, size_t size); @@ -145,14 +141,14 @@ class java_class_loadert:public messaget typedef optionalt> jar_index_optcreft; + jar_index_optcreft read_jar_file( - java_class_loader_limitt &class_loader_limit, const std::string &jar_path); + 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); + const jar_indext &jar_index); }; #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H