Skip to content

Commit 72fc31e

Browse files
author
thk123
committed
Add lazy version of load_java_class
This can be used to test the lazy behaviour of bytecode parsing
1 parent 5912a04 commit 72fc31e

File tree

2 files changed

+31
-0
lines changed

2 files changed

+31
-0
lines changed

unit/testing-utils/load_java_class.cpp

+26
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,32 @@
1818

1919
#include <java_bytecode/java_bytecode_language.h>
2020

21+
/// Go through the process of loading, type-checking and finalising loading a
22+
/// specific class file to build the symbol table. The functions are converted
23+
/// using ci_lazy_methods (equivalent to passing --lazy-methods to JBMC)
24+
/// \param java_class_name: The name of the class file to load. It should not
25+
/// include the .class extension.
26+
/// \param class_path: The path to load the class from. Should be relative to
27+
/// the unit directory.
28+
/// \param main: The name of the main function or "" to use the default
29+
/// behaviour to find a main function.
30+
/// \return The symbol table that is generated by parsing this file.
31+
symbol_tablet load_java_class_lazy(
32+
const std::string &java_class_name,
33+
const std::string &class_path,
34+
const std::string &main)
35+
{
36+
free_form_cmdlinet lazy_command_line;
37+
lazy_command_line.add_flag("lazy-methods");
38+
39+
return load_java_class(
40+
java_class_name,
41+
class_path,
42+
main,
43+
new_java_bytecode_language(),
44+
lazy_command_line);
45+
}
46+
2147
/// Go through the process of loading, type-checking and finalising loading a
2248
/// specific class file to build the symbol table.
2349
/// \param java_class_name: The name of the class file to load. It should not

unit/testing-utils/load_java_class.h

+5
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,9 @@ symbol_tablet load_java_class(
3838
std::unique_ptr<languaget> &&java_lang,
3939
const cmdlinet &command_line);
4040

41+
symbol_tablet load_java_class_lazy(
42+
const std::string &java_class_name,
43+
const std::string &class_path,
44+
const std::string &main);
45+
4146
#endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H

0 commit comments

Comments
 (0)