Skip to content

Commit 52379a8

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 1707b9d commit 52379a8

File tree

2 files changed

+32
-0
lines changed

2 files changed

+32
-0
lines changed

unit/testing-utils/load_java_class.cpp

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,33 @@
1818

1919
#include <java_bytecode/java_bytecode_language.h>
2020

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

unit/testing-utils/load_java_class.h

Lines changed: 5 additions & 0 deletions
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)