unify jar list and classpath

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -185,6 +185,12 @@ bool java_bytecode_languaget::parse(
   const std::string &path)
 {
   PRECONDITION(language_options_initialized);
+
+  java_class_loader.clear_classpath();
+
+  for(const auto &p : config.java.classpath)
+    java_class_loader.add_classpath_entry(p);
+
   java_class_loader.set_message_handler(get_message_handler());
   java_class_loader.set_java_cp_include_files(java_cp_include_files);
   java_class_loader.add_load_classes(java_load_classes);
@@ -232,7 +238,7 @@ bool java_bytecode_languaget::parse(
         main_jar_classes.push_back(kv.first);
     }
     else
-      java_class_loader.add_jar_file(path);
+      java_class_loader.add_classpath_entry(path);
   }
   else
     UNREACHABLE;

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -123,13 +123,14 @@ public:
       lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER),
       string_refinement_enabled(false),
       pointer_type_selector(std::move(pointer_type_selector))
-  {}
+  {
+  }
 
   java_bytecode_languaget():
     java_bytecode_languaget(
       std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
-  {}
-
+  {
+  }
 
   bool from_expr(
     const exprt &expr,

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/suffix.h>
 #include <util/prefix.h>
-#include <util/config.h>
 
 #include "java_bytecode_parser.h"
 
@@ -69,6 +68,11 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
   return class_map.at(class_name);
 }
 
+void java_class_loadert::add_classpath_entry(const std::string &path)
+{
+  classpath_entries.push_back(path);
+}
+
 optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   const irep_idt &class_name,
   const std::string &jar_file,
@@ -124,20 +128,8 @@ java_class_loadert::get_parse_tree(
     return parse_trees;
   }
 
-  // First add all given JAR files
-  for(const auto &jar_file : jar_files)
-  {
-    jar_index_optcreft index = read_jar_file(jar_file);
-    if(!index)
-      continue;
-    optionalt<java_bytecode_parse_treet> parse_tree =
-      get_class_from_jar(class_name, jar_file, *index);
-    if(parse_tree)
-      parse_trees.emplace_back(std::move(*parse_tree));
-  }
-
-  // Then add everything on the class path
-  for(const auto &cp_entry : config.java.classpath)
+  // Rummage through the class path
+  for(const auto &cp_entry : classpath_entries)
   {
     if(has_suffix(cp_entry, ".jar"))
     {
@@ -234,12 +226,12 @@ void java_class_loadert::load_entire_jar(
   if(!jar_index)
     return;
 
-  jar_files.push_front(jar_path);
+  classpath_entries.push_front(jar_path);
 
   for(const auto &e : jar_index->get())
     operator()(e.first);
 
-  jar_files.pop_front();
+  classpath_entries.pop_front();
 }
 
 java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(

jbmc/src/java_bytecode/java_class_loader.h

@@ -74,11 +74,19 @@ public:
     for(const auto &id : classes)
       java_load_classes.push_back(id);
   }
-  void add_jar_file(const std::string &f)
+
+  /// Clear all classpath entries
+  void clear_classpath()
   {
-    jar_files.push_back(f);
+    classpath_entries.clear();
   }
 
+  /// Appends an entry to the class path, used for loading classes.  The
+  /// argument may be
+  /// 1) The name of a directory, used for searching for .class files
+  /// 2) The name of a JAR file
+  void add_classpath_entry(const std::string &);
+
   static std::string file_to_class_name(const std::string &);
   static std::string class_name_to_file(const irep_idt &);
 
@@ -111,10 +119,8 @@ private:
   /// information.
   std::string java_cp_include_files;
 
-  /// List of filesystem paths to .jar files that will be used, in the given
-  /// order, to find and load a class, provided its name (see \ref
-  /// get_parse_tree).
-  std::list<std::string> jar_files;
+  /// List of entries in the classpath
+  std::list<std::string> classpath_entries;
 
   /// Classes to be explicitly loaded
   std::vector<irep_idt> java_load_classes;