1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
/*******************************************************************\
Module: Unit test utilities
Author: Diffblue Ltd.
\*******************************************************************/
/// \file
/// Helper functions for requiring specific types
/// If the type is of the wrong type, throw a CATCH exception
/// Also checks associated properties and returns a casted version of the
/// expression.
#ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
#define CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
#include <util/std_types.h>
#include <java_bytecode/java_types.h>
// NOLINTNEXTLINE(readability/namespace)
namespace require_type
{
pointer_typet
require_pointer(const typet &type, const std::optional<typet> &subtype);
#if defined(__GNUC__) && __GNUC__ >= 14
[[gnu::no_dangling]]
#endif
const struct_tag_typet &
require_struct_tag(const typet &type, const irep_idt &identifier = "");
pointer_typet require_pointer_to_tag(
const typet &type,
const irep_idt &identifier = irep_idt());
java_class_typet::componentt require_component(
const java_class_typet &java_class_type,
const irep_idt &component_name);
struct_typet::componentt require_component(
const struct_typet &struct_type,
const irep_idt &component_name);
code_typet require_code(const typet &type);
java_method_typet require_java_method(const typet &type);
code_typet::parametert
require_parameter(const code_typet &function_type, const irep_idt ¶m_name);
code_typet require_code(const typet &type, const size_t num_params);
java_method_typet
require_java_method(const typet &type, const size_t num_params);
// A mini DSL for describing an expected set of type arguments for a
// java_generic_typet
enum class type_argument_kindt
{
Inst,
Var
};
struct expected_type_argumentt
{
type_argument_kindt kind;
irep_idt description;
};
typedef std::initializer_list<expected_type_argumentt>
expected_type_argumentst;
java_generic_typet require_java_generic_type(const typet &type);
java_generic_typet require_java_generic_type(
const typet &type,
const require_type::expected_type_argumentst &type_expectations);
java_generic_parametert require_java_generic_parameter(const typet &type);
java_generic_parametert require_java_generic_parameter(
const typet &type,
const irep_idt ¶meter);
const typet &require_java_non_generic_type(
const typet &type,
const std::optional<struct_tag_typet> &expect_subtype);
class_typet require_complete_class(const typet &class_type);
class_typet require_incomplete_class(const typet &class_type);
java_generic_class_typet require_java_generic_class(const typet &class_type);
java_generic_class_typet require_java_generic_class(
const typet &class_type,
const std::initializer_list<irep_idt> &type_variables);
java_generic_class_typet
require_complete_java_generic_class(const typet &class_type);
java_generic_class_typet require_complete_java_generic_class(
const typet &class_type,
const std::initializer_list<irep_idt> &type_parameters);
java_implicitly_generic_class_typet
require_java_implicitly_generic_class(const typet &class_type);
java_implicitly_generic_class_typet require_java_implicitly_generic_class(
const typet &class_type,
const std::initializer_list<irep_idt> &implicit_type_variables);
java_implicitly_generic_class_typet
require_complete_java_implicitly_generic_class(const typet &class_type);
java_implicitly_generic_class_typet
require_complete_java_implicitly_generic_class(
const typet &class_type,
const std::initializer_list<irep_idt> &implicit_type_variables);
java_class_typet require_java_non_generic_class(const typet &class_type);
java_class_typet
require_complete_java_non_generic_class(const typet &class_type);
java_generic_struct_tag_typet require_java_generic_struct_tag_type(
const typet &type,
const std::string &identifier);
java_generic_struct_tag_typet require_java_generic_struct_tag_type(
const typet &type,
const std::string &identifier,
const require_type::expected_type_argumentst &type_expectations);
typedef java_class_typet::java_lambda_method_handlest
java_lambda_method_handlest;
java_lambda_method_handlest require_lambda_method_handles(
const java_class_typet &class_type,
const std::vector<std::string> &expected_identifiers);
}
#endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_TYPE_H
|
