Document the new class loading strategy for JARs

Author: antlechner

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -733,7 +733,12 @@ void janalyzer_parse_optionst::help()
     "Usage:                       Purpose:\n"
     "\n"
     " janalyzer [-?] [-h] [--help] show help\n"
-    " janalyzer class              name of class to be checked\n"
+    " janalyzer class              name of class or JAR file to be checked\n"
+    "                              In the case of a JAR file, if a main class can be\n" // NOLINT(*)
+    "                              inferred from --main-class, --function, or the JAR\n" // NOLINT(*)
+    "                              manifest (checked in this order), the behavior is\n" // NOLINT(*)
+    "                              the same as running janalyzer on the corresponding\n" // NOLINT(*)
+    "                              class file."
     "\n"
     "Task options:\n"
     " --show                       display the abstract domains\n"

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -168,6 +168,15 @@ bool java_bytecode_languaget::preprocess(
   return true;
 }
 
+/// We set the main class (i.e.\ class to start the class loading analysis from,
+/// see \ref java_class_loadert) depending on the file type of `path`.
+/// `path` can be the name of either a .class file or a .jar file.
+/// If it is a .class file, the top-level class in this file is the main class.
+/// If it is a .jar file, we first check for the main class in three steps
+/// 1) the argument of the --main-class command-line option,
+/// 2) the class implied by the argument of the --function option,
+/// 3) the manifest file of the JAR.
+/// If no main class was found, all classes in the JAR file are loaded.
 bool java_bytecode_languaget::parse(
   std::istream &,
   const std::string &path)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1018,7 +1018,12 @@ void jbmc_parse_optionst::help()
     "Usage:                       Purpose:\n"
     "\n"
     " jbmc [-?] [-h] [--help]      show help\n"
-    " jbmc class                   name of class to be checked\n"
+    " jbmc class                   name of class or JAR file to be checked\n"
+    "                              In the case of a JAR file, if a main class can be\n" // NOLINT(*)
+    "                              inferred from --main-class, --function, or the JAR\n" // NOLINT(*)
+    "                              manifest (checked in this order), the behavior is\n" // NOLINT(*)
+    "                              the same as running jbmc on the corresponding\n" // NOLINT(*)
+    "                              class file."
     "\n"
     "Analysis options:\n"
     HELP_SHOW_PROPERTIES