CBMC
|
Classes | |
struct | expected_instructiont |
Typedefs | |
typedef java_bytecode_parse_treet::classt::lambda_method_handlet | lambda_method_handlet |
typedef java_bytecode_parse_treet::methodt | methodt |
typedef std::vector< expected_instructiont > | expected_instructionst |
Functions | |
lambda_method_handlet | 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. More... | |
const methodt | 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. More... | |
void | 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. More... | |
typedef std::vector<expected_instructiont> require_parse_tree::expected_instructionst |
Definition at line 51 of file require_parse_tree.h.
typedef java_bytecode_parse_treet::classt::lambda_method_handlet require_parse_tree::lambda_method_handlet |
Definition at line 21 of file require_parse_tree.h.
Definition at line 27 of file require_parse_tree.h.
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.
expected_instructions | The expected instructions for a given method |
instructions | The instructions of a method |
Definition at line 79 of file require_parse_tree.cpp.
require_parse_tree::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.
Will fail if no matching lambda entry found.
parsed_class | the class to inspect |
lambda_method_ref | the reference/descriptor of the lambda method to which this lambda entry points to, must be unique |
Definition at line 23 of file require_parse_tree.cpp.
const require_parse_tree::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.
parsed_class | The class |
method_name | The name of the method to look for |
Definition at line 52 of file require_parse_tree.cpp.