cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
require_parse_tree.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Unit test utilities
4
5
Author: Diffblue Ltd.
6
7
\*******************************************************************/
8
9
#include "
require_parse_tree.h
"
10
11
#include <
testing-utils/use_catch.h
>
12
13
#include <iterator>
14
22
require_parse_tree::lambda_method_handlet
23
require_parse_tree::require_lambda_entry_for_descriptor
(
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);
31
const
irep_idt
method_ref_with_prefix =
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() ==
42
method_ref_with_prefix);
43
});
44
REQUIRE(matches.size() == 1);
45
return
matches.at(0).second;
46
}
47
52
const
require_parse_tree::methodt
require_parse_tree::require_method
(
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(),
59
[&method_name](
const
java_bytecode_parse_treet::methodt
&method) {
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
79
void
require_parse_tree::require_instructions_match_expectation
(
80
const
expected_instructionst
&expected_instructions,
81
const
java_bytecode_parse_treet::methodt::instructionst
instructions)
82
{
83
REQUIRE(instructions.size() == expected_instructions.size());
84
auto
actual_instruction_it = instructions.begin();
85
for
(
const
auto
&expected_instruction : expected_instructions)
86
{
87
expected_instruction.require_instructions_equal(*actual_instruction_it);
88
++actual_instruction_it;
89
}
90
}
91
94
void
require_parse_tree::expected_instructiont::require_instructions_equal
(
95
java_bytecode_parse_treet::instructiont
actual_instruction)
const
96
{
97
REQUIRE(
98
instruction_mnemoic
==
bytecode_info
[actual_instruction.
bytecode
].mnemonic);
99
REQUIRE(
instruction_arguments
.size() == actual_instruction.
args
.size());
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());
105
REQUIRE(*actual_arg_it == expected_arg);
106
++actual_arg_it;
107
}
108
}
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition
bytecode_info.cpp:16
exprt
Base class for all expressions.
Definition
expr.h:57
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition
irep.cpp:482
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
require_parse_tree::require_lambda_entry_for_descriptor
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...
Definition
require_parse_tree.cpp:23
require_parse_tree::lambda_method_handlet
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
Definition
require_parse_tree.h:21
require_parse_tree::expected_instructionst
std::vector< expected_instructiont > expected_instructionst
Definition
require_parse_tree.h:51
require_parse_tree::require_instructions_match_expectation
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.
Definition
require_parse_tree.cpp:79
require_parse_tree::methodt
java_bytecode_parse_treet::methodt methodt
Definition
require_parse_tree.h:27
require_parse_tree::require_method
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.
Definition
require_parse_tree.cpp:52
require_parse_tree.h
Utilties for inspecting java_parse_treet.
java_bytecode_parse_treet::classt
Definition
java_bytecode_parse_tree.h:197
java_bytecode_parse_treet::classt::methods
methodst methods
Definition
java_bytecode_parse_tree.h:280
java_bytecode_parse_treet::classt::lambda_method_handle_map
lambda_method_handle_mapt lambda_method_handle_map
Definition
java_bytecode_parse_tree.h:272
java_bytecode_parse_treet::instructiont
Definition
java_bytecode_parse_tree.h:56
java_bytecode_parse_treet::instructiont::args
argst args
Definition
java_bytecode_parse_tree.h:61
java_bytecode_parse_treet::instructiont::bytecode
u8 bytecode
Definition
java_bytecode_parse_tree.h:59
java_bytecode_parse_treet::methodt
Definition
java_bytecode_parse_tree.h:85
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition
java_bytecode_parse_tree.h:91
require_parse_tree::expected_instructiont::instruction_mnemoic
irep_idt instruction_mnemoic
Definition
require_parse_tree.h:47
require_parse_tree::expected_instructiont::require_instructions_equal
void require_instructions_equal(java_bytecode_parse_treet::instructiont actual_instruction) const
Check whether a given instruction matches an expectation of the instruction.
Definition
require_parse_tree.cpp:94
require_parse_tree::expected_instructiont::instruction_arguments
std::vector< exprt > instruction_arguments
Definition
require_parse_tree.h:48
use_catch.h
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
jbmc
unit
java-testing-utils
require_parse_tree.cpp
Generated by
1.17.0