Merge pull request #3052 from thk123/unit/add-load-java-class-goto-model-overload

Introduce overloads for getting a goto model out of load_java_class

Author: Daniel Kroening

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

@@ -18,8 +18,6 @@
 
 #include <goto-programs/lazy_goto_model.h>
 
-#include <langapi/mode.h>
-
 #include <java_bytecode/java_bytecode_language.h>
 #include <util/file_util.h>
 
@@ -38,42 +36,41 @@ symbol_tablet load_java_class_lazy(
   const std::string &class_path,
   const std::string &main)
 {
-  register_language(new_java_bytecode_language);
+  std::unique_ptr<languaget> lang = new_java_bytecode_language();
 
-  return load_java_class(
-    java_class_name, class_path, main, get_language_from_mode(ID_java));
+  return load_java_class(java_class_name, class_path, main, std::move(lang));
 }
 
-/// Go through the process of loading, type-checking and finalising loading a
-/// specific class file to build the symbol table.
-/// \param java_class_name: The name of the class file to load. It should not
-///   include the .class extension.
-/// \param class_path: The path to load the class from. Should be relative to
-///   the unit directory.
-/// \param main: The name of the main function or "" to use the default
-///   behaviour to find a main function.
-/// \return The symbol table that is generated by parsing this file.
+/// Returns the symbol table from
+/// \ref load_goto_model_from_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main) // NOLINT
 symbol_tablet load_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_symbol_table();
+}
 
-  return load_java_class(
-    java_class_name,
-    class_path,
-    main,
-    get_language_from_mode(ID_java),
-    command_line);
+/// Returns the symbol table from \ref load_goto_model_from_java_class
+symbol_tablet load_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)
+{
+  return load_goto_model_from_java_class(
+           java_class_name,
+           class_path,
+           main,
+           std::move(java_lang),
+           command_line)
+    .get_symbol_table();
 }
 
-/// Go through the process of loading, type-checking and finalising loading a
-/// specific class file to build the symbol table.
+/// Go through the process of loading, type-checking and finalising a
+/// specific class file to build a goto model from it.
 /// \param java_class_name: The name of the class file to load. It should not
 ///   include the .class extension.
 /// \param class_path: The path to load the class from. Should be relative to
@@ -82,8 +79,11 @@ symbol_tablet load_java_class(
 ///   behaviour to find a main function.
 /// \param java_lang: The language implementation to use for the loading,
 ///   which will be destroyed by this function.
-/// \return The symbol table that is generated by parsing this file.
-symbol_tablet load_java_class(
+/// \param command_line: The command line used to configure the provided
+///   language
+/// \return The goto model containing both the functions and the symbol table
+/// from loading this class.
+goto_modelt load_goto_model_from_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
   const std::string &main,
@@ -153,9 +153,12 @@ 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 std::move(*maybe_goto_model);
 }
 
+/// Returns the symbol table from \ref load_goto_model_from_java_class
+/// with the command line set to be disabling lazy loading and string
+/// refinement
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
@@ -173,3 +176,21 @@ symbol_tablet load_java_class(
   return load_java_class(
     java_class_name, class_path, main, std::move(java_lang), command_line);
 }
+
+/// See \ref load_goto_model_from_java_class
+/// With the command line configured to disable lazy loading and string
+/// refinement and the language set to be the default java_bytecode language
+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");
+
+  std::unique_ptr<languaget> lang = new_java_bytecode_language();
+
+  return load_goto_model_from_java_class(
+    java_class_name, class_path, main, std::move(lang), 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 = "");
 
+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);
 
+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,