CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
require_parse_tree.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_PARSE_TREE_H
13#define CPROVER_JAVA_TESTING_UTILS_REQUIRE_PARSE_TREE_H
14
16
17// NOLINTNEXTLINE(readability/namespace)
57
58#endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_PARSE_TREE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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 descrip...
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
std::vector< expected_instructiont > expected_instructionst
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.
java_bytecode_parse_treet::methodt methodt
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.
std::vector< instructiont > instructionst
expected_instructiont(const irep_idt &instruction_mnemoic, const std::vector< exprt > &instruction_arguments)
void require_instructions_equal(java_bytecode_parse_treet::instructiont actual_instruction) const
Check whether a given instruction matches an expectation of the instruction.