Document java_class_loader

Author: Matthias Güdemann

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -81,6 +81,11 @@ void java_class_loadert::add_classpath_entry(const std::string &path)
   }
 }
 
+/// Load class from jar file.
+/// \param class_name: name of class to load in Java source format
+/// \param jar_file: path of the jar file
+/// \param jar_index: the index of the jar file
+/// \return optional value of parse tree, empty if class cannot be loaded
 optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   const irep_idt &class_name,
   const std::string &jar_file,
@@ -102,6 +107,10 @@ optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   return java_bytecode_parse(istream, get_message_handler());
 }
 
+/// Check if class is an overlay class by inspecting the `ID_overlay_class`
+/// annotation.
+/// \param c: a `classt` object from a java byte code parse tree
+/// \return true if parsed class is an overlay class, else false
 static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
 {
   return java_bytecode_parse_treet::find_annotation(
@@ -228,6 +237,9 @@ 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`.
+/// \param jar_path: the path for the .jar to load
 void java_class_loadert::load_entire_jar(
   const std::string &jar_path)
 {
@@ -280,6 +292,12 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
   return std::cref(jar_index);
 }
 
+/// Convert a file name to the class name. Java interprets folders as packages,
+/// therefore a prefix of `./` is removed if necessary, and all `/` are
+/// converted to `.`. For example a class file `./com/diffblue/test.class` is
+/// converted to the class name `com.diffblue.test`.
+/// \param file: the name of the class file
+/// \return the file name converted to Java class name
 std::string java_class_loadert::file_to_class_name(const std::string &file)
 {
   std::string result=file;
@@ -307,6 +325,10 @@ std::string java_class_loadert::file_to_class_name(const std::string &file)
   return result;
 }
 
+/// Convert a class name to a file name, does the inverse of \ref
+/// file_to_class_name.
+/// \param class_name: the name of the class
+/// \return the class name converted to file name
 std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
 {
   std::string result=id2string(class_name);

jbmc/src/java_bytecode/java_class_loader.h

@@ -22,14 +22,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_parse_tree.h"
 #include "java_class_loader_limit.h"
 
+/// Class responsible to load .class files. Either directly from a specific
+/// file, from a classpath specification or from a Java archive (JAR) file.
 class java_class_loadert:public messaget
 {
 public:
   /// A map associating logical class names with the name of the .class file
   /// implementing it for all classes inside a single JAR file
   typedef std::map<irep_idt, std::string> jar_indext;
 
+  /// A list of parse trees supporting overlay classes
   typedef std::list<java_bytecode_parse_treet> parse_tree_with_overlayst;
+  /// A map from class names to list of parse tree where multiple entries can
+  /// exist in case of overlay classes.
   typedef std::map<irep_idt, parse_tree_with_overlayst>
     parse_tree_with_overridest_mapt;
 
@@ -54,6 +59,8 @@ class java_class_loadert:public messaget
     java_class_loader_limitt &class_loader_limit,
     const irep_idt &class_name);
 
+  /// Set the argument of the class loader limit \ref java_class_loader_limitt
+  /// \param java_cp_include_files: argument string for java_class_loader_limit
   void set_java_cp_include_files(const std::string &java_cp_include_files)
   {
     this->java_cp_include_files = java_cp_include_files;