CBMC
require_parse_tree Namespace Reference

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_instructiontexpected_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 Documentation

◆ expected_instructionst

◆ lambda_method_handlet

◆ methodt

Function Documentation

◆ require_instructions_match_expectation()

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.

Parameters
expected_instructionsThe expected instructions for a given method
instructionsThe instructions of a method

Definition at line 79 of file require_parse_tree.cpp.

◆ require_lambda_entry_for_descriptor()

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.

Parameters
parsed_classthe class to inspect
lambda_method_refthe reference/descriptor of the lambda method to which this lambda entry points to, must be unique
Returns

Definition at line 23 of file require_parse_tree.cpp.

◆ require_method()

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.

Parameters
parsed_classThe class
method_nameThe name of the method to look for
Returns
The methodt structure with the corresponding name

Definition at line 52 of file require_parse_tree.cpp.