@@ -65,12 +65,11 @@ code_typet require_type::require_code(const typet &type)
65
65
// / \param num_params check the the given code_typet expects this
66
66
// / number of parameters
67
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)
68
+ code_typet
69
+ require_type::require_code (const typet &type, const size_t num_params)
71
70
{
72
- code_typet code_type= require_code (type);
73
- REQUIRE (code_type.parameters ().size ()== num_params);
71
+ code_typet code_type = require_code (type);
72
+ REQUIRE (code_type.parameters ().size () == num_params);
74
73
return code_type;
75
74
}
76
75
@@ -105,82 +104,98 @@ bool require_java_generic_parametert_expectation(
105
104
{
106
105
switch (expected.kind )
107
106
{
108
- case require_type::type_parameter_kindt::Var:
109
- REQUIRE (!is_java_generic_inst_parameter ((param)));
110
- REQUIRE (param.type_variable ().get_identifier ()== expected.description );
111
- return true ;
112
- case require_type::type_parameter_kindt::Inst:
113
- REQUIRE (is_java_generic_inst_parameter ((param)));
114
- REQUIRE (param.subtype ()== symbol_typet (expected.description ));
115
- return true ;
107
+ case require_type::type_parameter_kindt::Var:
108
+ REQUIRE (!is_java_generic_inst_parameter ((param)));
109
+ REQUIRE (param.type_variable ().get_identifier () == expected.description );
110
+ return true ;
111
+ case require_type::type_parameter_kindt::Inst:
112
+ REQUIRE (is_java_generic_inst_parameter ((param)));
113
+ REQUIRE (param.subtype () == symbol_typet (expected.description ));
114
+ return true ;
116
115
}
117
116
// Should be unreachable...
118
117
REQUIRE (false );
119
118
return false ;
120
119
}
121
120
121
+ // / Verify a given type is a java_generic_type
122
+ // / \param type The type to check
123
+ // / \return The type, cast to a java_generic_typet
124
+ java_generic_typet require_type::require_java_generic_type (const typet &type)
125
+ {
126
+ REQUIRE (is_java_generic_type (type));
127
+ return to_java_generic_type (type);
128
+ }
122
129
123
- // / Verify a given type is a java_generic_type, optionally checking
130
+ // / Verify a given type is a java_generic_type, checking
124
131
// / that it's associated type variables match a given set of identifiers.
125
132
// / Expected usage is something like this:
126
133
// /
127
134
// / require_java_generic_type(type,
128
- // / {{Inst,"java::java.lang.Integer"},{Var,"T"}})
135
+ // / {{require_type::type_parameter_kindt::Inst, "java::java.lang.Integer"},
136
+ // / {require_type::type_parameter_kindt::Var, "T"}})
129
137
// /
130
138
// / \param type The type to check
131
- // / \param type_expectations An optional set of type variable kinds
139
+ // / \param type_expectations A set of type variable kinds
132
140
// / and identifiers which should be expected as the type parameters of the
133
141
// / given generic type.
134
142
// / \return The given type, cast to a java_generic_typet
135
143
java_generic_typet require_type::require_java_generic_type (
136
144
const typet &type,
137
- const optionalt< require_type::expected_type_parameterst> &type_expectations)
145
+ const require_type::expected_type_parameterst &type_expectations)
138
146
{
139
- REQUIRE (is_java_generic_type (type));
140
- const java_generic_typet &generic_type=to_java_generic_type (type);
141
- if (type_expectations)
142
- {
143
- const java_generic_typet::generic_type_variablest &generic_type_vars=
144
- generic_type.generic_type_variables ();
145
- REQUIRE (generic_type_vars.size ()==type_expectations->size ());
146
- REQUIRE (
147
- std::equal (
148
- generic_type_vars.begin (),
149
- generic_type_vars.end (),
150
- type_expectations->begin (),
151
- require_java_generic_parametert_expectation));
152
- }
147
+ const java_generic_typet &generic_type =
148
+ require_type::require_java_generic_type (type);
149
+
150
+ const java_generic_typet::generic_type_variablest &generic_type_vars =
151
+ generic_type.generic_type_variables ();
152
+ REQUIRE (generic_type_vars.size () == type_expectations.size ());
153
+ REQUIRE (
154
+ std::equal (
155
+ generic_type_vars.begin (),
156
+ generic_type_vars.end (),
157
+ type_expectations.begin (),
158
+ require_java_generic_parametert_expectation));
153
159
154
160
return generic_type;
155
161
}
156
162
157
- // / Verify a given type is a java_generic_parameter, optionally checking
163
+ // / Verify a given type is a java_generic_parameter
164
+ // / \param type The type to check
165
+ // / \return The type, cast to a java_generic_parametert
166
+ java_generic_parametert
167
+ require_type::require_java_generic_parameter (const typet &type)
168
+ {
169
+ REQUIRE (is_java_generic_parameter (type));
170
+ return to_java_generic_parameter (type);
171
+ }
172
+
173
+ // / Verify a given type is a java_generic_parameter, checking
158
174
// / that it's associated type variables match a given set of expectations.
159
175
// / Expected usage is something like this:
160
176
// /
161
- // / require_java_generic_parameter(parameter, {Inst,"java::java.lang.Integer"})
177
+ // / require_java_generic_parameter(parameter,
178
+ // / {require_type::type_parameter_kindt::Inst,"java::java.lang.Integer"})
162
179
// /
163
180
// / or
164
181
// /
165
- // / require_java_generic_parameter(parameter, {Var,"T"})
182
+ // / require_java_generic_parameter(parameter,
183
+ // / {require_type::type_parameter_kindt::Var,"T"})
166
184
// /
167
185
// / \param type The type to check
168
- // / \param type_expectation An optional description of the identifiers/kinds
186
+ // / \param type_expectation A description of the identifiers/kinds
169
187
// / which / should be expected as the type parameter of the generic parameter.
170
188
// / \return The given type, cast to a java_generic_parametert
171
189
java_generic_parametert require_type::require_java_generic_parameter (
172
190
const typet &type,
173
- const optionalt< require_type::expected_type_parametert> &type_expectation)
191
+ const require_type::expected_type_parametert &type_expectation)
174
192
{
175
- REQUIRE (is_java_generic_parameter (type));
176
- const java_generic_parametert &generic_param=to_java_generic_parameter (type);
177
- if (type_expectation)
178
- {
179
- REQUIRE (
180
- require_java_generic_parametert_expectation (
181
- generic_param,
182
- type_expectation.value ()));
183
- }
193
+ const java_generic_parametert &generic_param =
194
+ require_type::require_java_generic_parameter (type);
195
+
196
+ REQUIRE (
197
+ require_java_generic_parametert_expectation (
198
+ generic_param, type_expectation));
184
199
185
200
return generic_param;
186
201
}
@@ -198,7 +213,7 @@ const typet &require_type::require_java_non_generic_type(
198
213
REQUIRE (!is_java_generic_type (type));
199
214
REQUIRE (!is_java_generic_inst_parameter (type));
200
215
if (expect_subtype)
201
- REQUIRE (type.subtype ()== expect_subtype.value ());
216
+ REQUIRE (type.subtype () == expect_subtype.value ());
202
217
return type;
203
218
}
204
219
@@ -216,14 +231,11 @@ class_typet require_complete_class(const typet &class_type)
216
231
return class_class_type;
217
232
}
218
233
219
- // / Verify that a class is a complete, valid java generic class with the
220
- // / specified list of variables.
234
+ // / Verify that a class is a complete, valid java generic class.
221
235
// / \param class_type: the class
222
- // / \param type_variables: vector of type variables
223
236
// / \return: A reference to the java generic class type.
224
- java_generics_class_typet require_type::require_java_generic_class (
225
- const typet &class_type,
226
- const optionalt<std::initializer_list<irep_idt>> &type_variables)
237
+ java_generics_class_typet
238
+ require_type::require_java_generic_class (const typet &class_type)
227
239
{
228
240
const class_typet &class_class_type = require_complete_class (class_type);
229
241
java_class_typet java_class_type = to_java_class_type (class_class_type);
@@ -232,22 +244,35 @@ java_generics_class_typet require_type::require_java_generic_class(
232
244
java_generics_class_typet java_generic_class_type =
233
245
to_java_generics_class_type (java_class_type);
234
246
235
- if (type_variables)
236
- {
237
- const java_generics_class_typet::generic_typest &generic_type_vars =
238
- java_generic_class_type.generic_types ();
239
- REQUIRE (generic_type_vars.size () == type_variables.value ().size ());
240
- REQUIRE (
241
- std::equal (
242
- type_variables->begin (),
243
- type_variables->end (),
244
- generic_type_vars.begin (),
245
- [](
246
- const irep_idt &type_var_name, const java_generic_parametert ¶m) {
247
- REQUIRE (!is_java_generic_inst_parameter ((param)));
248
- return param.type_variable ().get_identifier () == type_var_name;
249
- }));
250
- }
247
+ return java_generic_class_type;
248
+ }
249
+
250
+ // / Verify that a class is a complete, valid java generic class with the
251
+ // / specified list of variables.
252
+ // / \param class_type: the class
253
+ // / \param type_variables: vector of type variables
254
+ // / \return: A reference to the java generic class type.
255
+ java_generics_class_typet require_type::require_java_generic_class (
256
+ const typet &class_type,
257
+ const std::initializer_list<irep_idt> &type_variables)
258
+ {
259
+ const java_generics_class_typet java_generic_class_type =
260
+ require_type::require_java_generic_class (class_type);
261
+
262
+ const java_generics_class_typet::generic_typest &generic_type_vars =
263
+ java_generic_class_type.generic_types ();
264
+ REQUIRE (generic_type_vars.size () == type_variables.size ());
265
+ REQUIRE (
266
+ std::equal (
267
+ type_variables.begin (),
268
+ type_variables.end (),
269
+ generic_type_vars.begin (),
270
+ [](const irep_idt &type_var_name, const java_generic_parametert ¶m)
271
+ {
272
+ REQUIRE (!is_java_generic_inst_parameter ((param)));
273
+ return param.type_variable ().get_identifier () == type_var_name;
274
+ }));
275
+
251
276
return java_generic_class_type;
252
277
}
253
278
0 commit comments