java_class_loadert::load_entire_jar now returns the classes loaded

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -235,9 +235,9 @@ 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(path);
-      for(const auto &kv : java_class_loader.get_jar_index(path))
-        main_jar_classes.push_back(kv.first);
+      const auto classes = java_class_loader.load_entire_jar(path);
+      for(const auto &c : classes)
+        main_jar_classes.push_back(c);
     }
     else
       java_class_loader.add_classpath_entry(path);

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -238,23 +238,29 @@ java_class_loadert::get_parse_tree(
   return parse_trees;
 }
 
-/// Load all class files from a .jar file, and store name of .jar in
-/// `classpath_entreies`.
+/// Load all class files from a .jar file
 /// \param jar_path: the path for the .jar to load
-void java_class_loadert::load_entire_jar(
+std::vector<irep_idt> java_class_loadert::load_entire_jar(
   const std::string &jar_path)
 {
   jar_index_optcreft jar_index = read_jar_file(jar_path);
   if(!jar_index)
-    return;
+    return {};
 
   classpath_entries.push_front(
     classpath_entryt(classpath_entryt::JAR, jar_path));
 
+  std::vector<irep_idt> classes;
+
   for(const auto &e : jar_index->get())
+  {
     operator()(e.first);
+    classes.push_back(e.first);
+  }
 
   classpath_entries.pop_front();
+
+  return classes;
 }
 
 java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(

jbmc/src/java_bytecode/java_class_loader.h

@@ -97,7 +97,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(const std::string &jar_path);
+  std::vector<irep_idt> load_entire_jar(const std::string &jar_path);
 
   const jar_indext &get_jar_index(const std::string &jar_path)
   {