@@ -59,6 +59,21 @@ code_typet require_type::require_code(const typet &type)
59
59
return to_code_type (type);
60
60
}
61
61
62
+ // / Verify a given type is an code_typet, and that the code it represents
63
+ // / accepts a given number of parameters
64
+ // / \param type The type to check
65
+ // / \param num_params check the the given code_typet expects this
66
+ // / number of parameters
67
+ // / \return The type cast to a code_typet
68
+ code_typet require_type::require_code (
69
+ const typet &type,
70
+ const size_t num_params)
71
+ {
72
+ code_typet code_type=require_code (type);
73
+ REQUIRE (code_type.parameters ().size ()==num_params);
74
+ return code_type;
75
+ }
76
+
62
77
// / Verify that a function has a parameter of a specific name.
63
78
// / \param function_type: The type of the function
64
79
// / \param param_name: The name of the parameter
@@ -78,3 +93,105 @@ code_typet::parametert require_type::require_parameter(
78
93
REQUIRE (param != function_type.parameters ().end ());
79
94
return *param;
80
95
}
96
+
97
+ // / Verify a given type is a java_generic_type, optionally checking
98
+ // / that it's associated type variables match a given set of identifiers
99
+ // / \param type The type to check
100
+ // / \param type_variables An optional set of type variable identifiers which
101
+ // / should be expected as the type parameters of the generic type.
102
+ // / \return The given type, cast to a java_generic_typet
103
+ const java_generic_typet &require_type::require_java_generic_type_variables (
104
+ const typet &type,
105
+ const optionalt<std::initializer_list<irep_idt>> &type_variables)
106
+ {
107
+ REQUIRE (is_java_generic_type (type));
108
+ const java_generic_typet &generic_type=to_java_generic_type (type);
109
+ if (type_variables)
110
+ {
111
+ const java_generic_typet::generic_type_variablest &generic_type_vars=
112
+ generic_type.generic_type_variables ();
113
+ REQUIRE (generic_type_vars.size ()==type_variables.value ().size ());
114
+ REQUIRE (
115
+ std::equal (
116
+ type_variables->begin (),
117
+ type_variables->end (),
118
+ generic_type_vars.begin (),
119
+ [](const irep_idt &type_var_name, const java_generic_parametert ¶m)
120
+ {
121
+ REQUIRE (!is_java_generic_inst_parameter ((param)));
122
+ return param.type_variable ().get_identifier ()==type_var_name;
123
+ }));
124
+ }
125
+
126
+ return generic_type;
127
+ }
128
+
129
+ // / Verify a given type is a java_generic_type, optionally checking
130
+ // / that it's associated type variables match a given set of identifiers
131
+ // / \param type The type to check
132
+ // / \param type_variables An optional set of type variable identifiers which
133
+ // / should be expected as the type parameters of the generic type.
134
+ // / \return The given type, cast to a java_generic_typet
135
+ const java_generic_typet
136
+ &require_type::require_java_generic_type_instantiations (
137
+ const typet &type,
138
+ const optionalt<std::initializer_list<irep_idt>> &type_instantiations)
139
+ {
140
+ REQUIRE (is_java_generic_type (type));
141
+ const java_generic_typet &generic_type=to_java_generic_type (type);
142
+ if (type_instantiations)
143
+ {
144
+ const java_generic_typet::generic_type_variablest &generic_type_vars=
145
+ generic_type.generic_type_variables ();
146
+ REQUIRE (generic_type_vars.size ()==type_instantiations.value ().size ());
147
+ REQUIRE (
148
+ std::equal (
149
+ type_instantiations->begin (),
150
+ type_instantiations->end (),
151
+ generic_type_vars.begin (),
152
+ [](const irep_idt &type_id, const java_generic_parametert ¶m)
153
+ {
154
+ REQUIRE (is_java_generic_inst_parameter ((param)));
155
+ return param.subtype ()==symbol_typet (type_id);
156
+ }));
157
+ }
158
+
159
+
160
+ return generic_type;
161
+ }
162
+
163
+ // / Verify a given type is a java_generic_parameter, optionally checking
164
+ // / that it's associated type variables match a given set of identifiers
165
+ // / \param type The type to check
166
+ // / \param type_variables An optional set of type variable identifiers which
167
+ // / should be expected as the type parameters of the generic type.
168
+ // / \return The given type, cast to a java_generic_typet
169
+ const java_generic_parametert
170
+ &require_type::require_java_generic_parameter_variables (
171
+ const typet &type,
172
+ const optionalt<irep_idt> &type_variable)
173
+ {
174
+ REQUIRE (is_java_generic_parameter (type));
175
+ const java_generic_parametert &generic_param=to_java_generic_parameter (type);
176
+ if (type_variable)
177
+ {
178
+ const java_generic_parametert::type_variablet &generic_type_var=
179
+ generic_param.type_variable ();
180
+ REQUIRE (!is_java_generic_inst_parameter ((generic_param)));
181
+ REQUIRE (generic_type_var.get_identifier ()==type_variable.value ());
182
+ }
183
+
184
+ return generic_param;
185
+ }
186
+
187
+ const typet &require_type::require_java_non_generic_type (
188
+ const typet &type,
189
+ const optionalt<irep_idt> &expect_type)
190
+ {
191
+ REQUIRE (!is_java_generic_parameter (type));
192
+ REQUIRE (!is_java_generic_type (type));
193
+ REQUIRE (!is_java_generic_inst_parameter (type));
194
+ if (expect_type)
195
+ REQUIRE (type.subtype ()==symbol_typet (expect_type.value ()));
196
+ return type;
197
+ }
0 commit comments