diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 45ccd69ec7b..659842f178f 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,5 +1,6 @@ SRC = \ c_to_expr.cpp \ + free_form_cmdline.cpp \ load_java_class.cpp \ require_expr.cpp \ require_goto_statements.cpp \ diff --git a/unit/testing-utils/free_form_cmdline.cpp b/unit/testing-utils/free_form_cmdline.cpp new file mode 100644 index 00000000000..3b310f4d139 --- /dev/null +++ b/unit/testing-utils/free_form_cmdline.cpp @@ -0,0 +1,35 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. + +\*******************************************************************/ + +#include "free_form_cmdline.h" + +/// Create a command line option that can be set +/// \param flag_name: The name of the command line option to support +void free_form_cmdlinet::create_flag(const std::string &flag_name) +{ + optiont option; + option.optstring = flag_name; + options.push_back(option); +} + +/// Equivalent to specifying --flag for the command line +/// \param flag: The name of the flag to specify +void free_form_cmdlinet::add_flag(std::string flag) +{ + create_flag(flag); + set(flag); +} + +/// Equivalent to specifying --flag value +/// \param flag: The name of the flag to specify +/// \param value: The value to the set the command line option to +void free_form_cmdlinet::add_option(std::string flag, std::string value) +{ + create_flag(flag); + set(flag, value); +} diff --git a/unit/testing-utils/free_form_cmdline.h b/unit/testing-utils/free_form_cmdline.h new file mode 100644 index 00000000000..040099d3cd7 --- /dev/null +++ b/unit/testing-utils/free_form_cmdline.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. + +\*******************************************************************/ + +#ifndef CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H +#define CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H + +#include + +/// An implementation of cmdlinet to be used in tests. It does not require +/// specifying exactly what flags are supported and instead allows setting any +/// flag +class free_form_cmdlinet : public cmdlinet +{ +public: + void add_flag(std::string flag); + void add_option(std::string flag, std::string value); + +private: + void create_flag(const std::string &flag_name); +}; + +#endif // CPROVER_TESTING_UTILS_FREE_FORM_CMDLINE_H diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index 38ef466e8f2..82521b9eff6 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -7,17 +7,43 @@ \*******************************************************************/ #include "load_java_class.h" +#include "free_form_cmdline.h" #include #include #include -#include #include #include #include +/// Go through the process of loading, type-checking and finalising loading a +/// specific class file to build the symbol table. The functions are converted +/// using ci_lazy_methods (equivalent to passing --lazy-methods to JBMC) +/// \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. +symbol_tablet load_java_class_lazy( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main) +{ + free_form_cmdlinet lazy_command_line; + lazy_command_line.add_flag("lazy-methods"); + + return load_java_class( + java_class_name, + class_path, + main, + new_java_bytecode_language(), + lazy_command_line); +} + /// 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 @@ -51,7 +77,8 @@ symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, const std::string &main, - std::unique_ptr &&java_lang) + std::unique_ptr &&java_lang, + const cmdlinet &command_line) { // We expect the name of the class without the .class suffix to allow us to // check it @@ -66,8 +93,6 @@ symbol_tablet load_java_class( message_handler); // Configure the path loading - cmdlinet command_line; - command_line.set("java-cp-include-files", class_path); config.java.classpath.clear(); config.java.classpath.push_back(class_path); config.main = main; @@ -109,3 +134,19 @@ symbol_tablet load_java_class( REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); return std::move(maybe_goto_model->symbol_table); } + +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main, + std::unique_ptr &&java_lang) +{ + cmdlinet command_line; + // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an + // TODO(tkiley): unknown argument. This could be changed by using the + // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail. + // TODO(tkiley): TG-2708 to investigate and fix + command_line.set("java-cp-include-files", class_path); + return load_java_class( + java_class_name, class_path, main, std::move(java_lang), command_line); +} diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index 01cd3bfda16..0a29a2304aa 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -18,6 +18,7 @@ #include #include +#include symbol_tablet load_java_class( const std::string &java_class_name, @@ -30,4 +31,16 @@ symbol_tablet load_java_class( const std::string &main, std::unique_ptr &&java_lang); +symbol_tablet load_java_class( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main, + std::unique_ptr &&java_lang, + const cmdlinet &command_line); + +symbol_tablet load_java_class_lazy( + const std::string &java_class_name, + const std::string &class_path, + const std::string &main); + #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H