Introduce overloads for getting a goto model out of load_java_class

This can be used when you need both the symbol table and the goto
functions map, or when you have whole goto_model passes.

Author: thk123

jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -58,18 +58,8 @@ symbol_tablet load_java_class(
   const std::string &class_path,
   const std::string &main)
 {
-  free_form_cmdlinet command_line;
-  command_line.add_flag("no-lazy-methods");
-  command_line.add_flag("no-refine-strings");
-
-  register_language(new_java_bytecode_language);
-
-  return load_java_class(
-    java_class_name,
-    class_path,
-    main,
-    get_language_from_mode(ID_java),
-    command_line);
+  return load_goto_model_from_java_class(java_class_name, class_path, main)
+    ->get_symbol_table();
 }
 
 /// Go through the process of loading, type-checking and finalising loading a
@@ -89,6 +79,22 @@ symbol_tablet load_java_class(
   const std::string &main,
   std::unique_ptr<languaget> &&java_lang,
   const cmdlinet &command_line)
+{
+  return load_goto_model_from_java_class(
+           java_class_name,
+           class_path,
+           main,
+           std::move(java_lang),
+           command_line)
+    ->get_symbol_table();
+}
+
+std::unique_ptr<goto_modelt> load_goto_model_from_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main,
+  std::unique_ptr<languaget> &&java_lang,
+  const cmdlinet &command_line)
 {
   // We expect the name of the class without the .class suffix to allow us to
   // check it
@@ -153,7 +159,7 @@ symbol_tablet load_java_class(
   // Check your working directory and the class path is correctly configured
   // as this often indicates that one of these is wrong.
   REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
-  return std::move(maybe_goto_model->symbol_table);
+  return maybe_goto_model;
 }
 
 symbol_tablet load_java_class(
@@ -173,3 +179,22 @@ symbol_tablet load_java_class(
   return load_java_class(
     java_class_name, class_path, main, std::move(java_lang), command_line);
 }
+
+std::unique_ptr<goto_modelt> load_goto_model_from_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main)
+{
+  free_form_cmdlinet command_line;
+  command_line.add_flag("no-lazy-methods");
+  command_line.add_flag("no-refine-strings");
+
+  register_language(new_java_bytecode_language);
+
+  return load_goto_model_from_java_class(
+    java_class_name,
+    class_path,
+    main,
+    get_language_from_mode(ID_java),
+    command_line);
+}

jbmc/unit/java-testing-utils/load_java_class.h

@@ -25,6 +25,11 @@ symbol_tablet load_java_class(
   const std::string &class_path,
   const std::string &main = "");
 
+std::unique_ptr<goto_modelt> load_goto_model_from_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main = "");
+
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
@@ -38,6 +43,13 @@ symbol_tablet load_java_class(
   std::unique_ptr<languaget> &&java_lang,
   const cmdlinet &command_line);
 
+std::unique_ptr<goto_modelt> load_goto_model_from_java_class(
+  const std::string &java_class_name,
+  const std::string &class_path,
+  const std::string &main,
+  std::unique_ptr<languaget> &&java_lang,
+  const cmdlinet &command_line);
+
 symbol_tablet load_java_class_lazy(
   const std::string &java_class_name,
   const std::string &class_path,