Skip to content

Commit c2baf1b

Browse files
committed
Split load_goto_model_from_java_class into two functions
The new overload allows specifying the command-line options to run jbmc with. For example, we will be able to specify that --context-include should be used.
1 parent e3f6972 commit c2baf1b

File tree

2 files changed

+31
-5
lines changed

2 files changed

+31
-5
lines changed

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

Lines changed: 22 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -179,20 +179,37 @@ symbol_tablet load_java_class(
179179
java_class_name, class_path, main, std::move(java_lang), command_line);
180180
}
181181

182-
/// See \ref load_goto_model_from_java_class
183-
/// With the command line configured to disable lazy loading and string
184-
/// refinement and the language set to be the default java_bytecode language
185182
goto_modelt load_goto_model_from_java_class(
186183
const std::string &java_class_name,
187184
const std::string &class_path,
185+
const std::vector<std::string> &command_line_flags,
186+
const std::unordered_map<std::string, std::string> &command_line_options,
188187
const std::string &main)
189188
{
190189
free_form_cmdlinet command_line;
191-
command_line.add_flag("no-lazy-methods");
192-
command_line.add_flag("no-refine-strings");
190+
for(const auto &flag : command_line_flags)
191+
command_line.add_flag(flag);
192+
for(const auto &option : command_line_options)
193+
command_line.add_option(option.first, option.second);
193194

194195
std::unique_ptr<languaget> lang = new_java_bytecode_language();
195196

196197
return load_goto_model_from_java_class(
197198
java_class_name, class_path, main, std::move(lang), command_line);
198199
}
200+
201+
/// See \ref load_goto_model_from_java_class
202+
/// With the command line configured to disable lazy loading and string
203+
/// refinement and the language set to be the default java_bytecode language
204+
goto_modelt load_goto_model_from_java_class(
205+
const std::string &java_class_name,
206+
const std::string &class_path,
207+
const std::string &main)
208+
{
209+
return load_goto_model_from_java_class(
210+
java_class_name,
211+
class_path,
212+
{"no-lazy-methods", "no-refine-strings"},
213+
{},
214+
main);
215+
}

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,15 @@ symbol_tablet load_java_class_lazy(
5050
const std::string &class_path,
5151
const std::string &main);
5252

53+
/// Overload of load_goto_model_from_java_class with configurable command-line
54+
/// options.
55+
goto_modelt load_goto_model_from_java_class(
56+
const std::string &java_class_name,
57+
const std::string &class_path,
58+
const std::vector<std::string> &command_line_flags,
59+
const std::unordered_map<std::string, std::string> &command_line_options,
60+
const std::string &main = "");
61+
5362
goto_modelt load_goto_model_from_java_class(
5463
const std::string &java_class_name,
5564
const std::string &class_path,

0 commit comments

Comments
 (0)