CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
require_parse_tree.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
12
13#include <iterator>
14
24 const java_bytecode_parse_treet::classt &parsed_class,
25 const std::string &lambda_method_ref)
26{
27 typedef java_bytecode_parse_treet::classt::lambda_method_handle_mapt::
28 value_type lambda_method_entryt;
29
30 INFO("Looking for entry with lambda_method_ref: " << lambda_method_ref);
32 "java::" + id2string(lambda_method_ref);
33
34 std::vector<lambda_method_entryt> matches;
35 std::copy_if(
36 parsed_class.lambda_method_handle_map.begin(),
37 parsed_class.lambda_method_handle_map.end(),
38 back_inserter(matches),
39 [&method_ref_with_prefix](const lambda_method_entryt &entry) { //NOLINT
40 return (
41 entry.second.get_method_descriptor().get_identifier() ==
43 });
44 REQUIRE(matches.size() == 1);
45 return matches.at(0).second;
46}
47
53 const java_bytecode_parse_treet::classt &parsed_class,
54 const irep_idt &method_name)
55{
56 const auto method = std::find_if(
57 parsed_class.methods.begin(),
58 parsed_class.methods.end(),
60 return method.name == method_name;
61 });
62
63 INFO("Looking for method: " << method_name);
64 std::ostringstream found_methods;
65 for(const auto &entry : parsed_class.methods)
66 {
67 found_methods << id2string(entry.name) << std::endl;
68 }
69 INFO("Found methods:\n" << found_methods.str());
70
71 REQUIRE(method != parsed_class.methods.end());
72
73 return *method;
74}
75
91
96{
97 REQUIRE(
100 auto actual_arg_it = actual_instruction.args.begin();
101 for(const exprt &expected_arg : actual_instruction.args)
102 {
103 INFO("Expected argument" << expected_arg.pretty());
104 INFO("Actual argument" << actual_arg_it->pretty());
107 }
108}
struct bytecode_infot const bytecode_info[]
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
Base class for all expressions.
Definition expr.h:56
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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...
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.
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.
Utilties for inspecting java_parse_treet.
lambda_method_handle_mapt lambda_method_handle_map
std::vector< instructiont > instructionst
void require_instructions_equal(java_bytecode_parse_treet::instructiont actual_instruction) const
Check whether a given instruction matches an expectation of the instruction.