CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
require_parse_tree.h File Reference

Utilties for inspecting java_parse_treet. More...

+ Include dependency graph for require_parse_tree.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  require_parse_tree::expected_instructiont
 

Namespaces

namespace  require_parse_tree
 

Typedefs

typedef java_bytecode_parse_treet::classt::lambda_method_handlet require_parse_tree::lambda_method_handlet
 
typedef java_bytecode_parse_treet::methodt require_parse_tree::methodt
 
typedef std::vector< expected_instructiontrequire_parse_tree::expected_instructionst
 

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.
 

Detailed Description

Utilties for inspecting java_parse_treet.

Definition in file require_parse_tree.h.