Add new option --ignore-manifest-main-class

If the option is specified, any main class that may be specified in the
manifest file of a JAR will be ignored in the class loading stage.
This is useful when we want to e.g. load all classes in a JAR file, some
of which may not be referenced from the specified main class.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -69,6 +69,9 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
   options.set_option(
     "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
 
+  options.set_option(
+    "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
+
   if(cmd.isset("context-include"))
     options.set_option("context-include", cmd.get_values("context-include"));
 
@@ -201,6 +204,9 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
   nondet_static = options.get_bool_option("nondet-static");
   static_values_file = options.get_option("static-values");
 
+  ignore_manifest_main_class =
+    options.get_bool_option("ignore-manifest-main-class");
+
   if(options.is_set("context-include") || options.is_set("context-exclude"))
     method_in_context = get_context(options);
 
@@ -288,7 +294,7 @@ bool java_bytecode_languaget::parse(
         std::string manifest_main_class = manifest["Main-Class"];
 
         // if the manifest declares a Main-Class line, we got a main class
-        if(!manifest_main_class.empty())
+        if(!manifest_main_class.empty() && !ignore_manifest_main_class)
           main_class = manifest_main_class;
       }
     }

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -40,6 +40,7 @@ Author: Daniel Kroening, [email protected]
   "(max-nondet-tree-depth):" \
   "(java-max-vla-length):" \
   "(java-cp-include-files):" \
+  "(ignore-manifest-main-class)" \
   "(context-include):" \
   "(context-exclude):" \
   "(no-lazy-methods)" \
@@ -73,6 +74,11 @@ Author: Daniel Kroening, [email protected]
   " --java-max-vla-length N      limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
   " --java-cp-include-files r    regexp or JSON list of files to load\n" \
   "                              (with '@' prefix)\n" \
+  " --ignore-manifest-main-class ignore Main-Class entries in JAR manifest files.\n" /* NOLINT(*) */ \
+  "                              If this option is specified and the options\n" /* NOLINT(*) */ \
+  "                              --function and --main-class are not, we can be\n" /* NOLINT(*) */ \
+  "                              certain that all classes in the JAR file are\n" /* NOLINT(*) */ \
+  "                              loaded." \
   " --context-include i          only analyze code matching specification i that\n" /* NOLINT(*) */ \
   " --context-exclude e          does not match specification e.\n" \
   "                              A specification is any prefix of a package, class\n" /* NOLINT(*) */ \
@@ -215,6 +221,7 @@ class java_bytecode_languaget:public languaget
   bool language_options_initialized;
   irep_idt main_class;
   std::vector<irep_idt> main_jar_classes;
+  bool ignore_manifest_main_class;
   java_class_loadert java_class_loader;
   bool threading_support;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null