CBMC
|
Utilties for inspecting java_parse_treet. More...
#include <java_bytecode/java_bytecode_parse_tree.h>
Go to the source code of this file.
Classes | |
struct | require_parse_tree::expected_instructiont |
Namespaces | |
namespace | require_parse_tree |
Functions | |
lambda_method_handlet | require_parse_tree::require_lambda_entry_for_descriptor (const java_bytecode_parse_treet::classt &parsed_class, const std::string &lambda_method_ref) |
Find in the parsed class a specific entry within the lambda_method_handle_map with a matching descriptor. | |
const methodt | require_parse_tree::require_method (const java_bytecode_parse_treet::classt &parsed_class, const irep_idt &method_name) |
Finds a specific method in the parsed class with a matching name. | |
void | require_parse_tree::require_instructions_match_expectation (const expected_instructionst &expected_instructions, const java_bytecode_parse_treet::methodt::instructionst instructions) |
Verify whether a given methods instructions match an expectation. | |
Utilties for inspecting java_parse_treet.
Definition in file require_parse_tree.h.