@@ -65,12 +65,11 @@ code_typet require_type::require_code(const typet &type)
6565// / \param num_params check the the given code_typet expects this
6666// / number of parameters
6767// / \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)
7170{
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);
7473 return code_type;
7574}
7675
@@ -105,82 +104,98 @@ bool require_java_generic_parametert_expectation(
105104{
106105 switch (expected.kind )
107106 {
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 ;
116115 }
117116 // Should be unreachable...
118117 REQUIRE (false );
119118 return false ;
120119}
121120
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+ }
122129
123- // / Verify a given type is a java_generic_type, optionally checking
130+ // / Verify a given type is a java_generic_type, checking
124131// / that it's associated type variables match a given set of identifiers.
125132// / Expected usage is something like this:
126133// /
127134// / 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"}})
129137// /
130138// / \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
132140// / and identifiers which should be expected as the type parameters of the
133141// / given generic type.
134142// / \return The given type, cast to a java_generic_typet
135143java_generic_typet require_type::require_java_generic_type (
136144 const typet &type,
137- const optionalt< require_type::expected_type_parameterst> &type_expectations)
145+ const require_type::expected_type_parameterst &type_expectations)
138146{
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));
153159
154160 return generic_type;
155161}
156162
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
158174// / that it's associated type variables match a given set of expectations.
159175// / Expected usage is something like this:
160176// /
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"})
162179// /
163180// / or
164181// /
165- // / require_java_generic_parameter(parameter, {Var,"T"})
182+ // / require_java_generic_parameter(parameter,
183+ // / {require_type::type_parameter_kindt::Var,"T"})
166184// /
167185// / \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
169187// / which / should be expected as the type parameter of the generic parameter.
170188// / \return The given type, cast to a java_generic_parametert
171189java_generic_parametert require_type::require_java_generic_parameter (
172190 const typet &type,
173- const optionalt< require_type::expected_type_parametert> &type_expectation)
191+ const require_type::expected_type_parametert &type_expectation)
174192{
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));
184199
185200 return generic_param;
186201}
@@ -198,7 +213,7 @@ const typet &require_type::require_java_non_generic_type(
198213 REQUIRE (!is_java_generic_type (type));
199214 REQUIRE (!is_java_generic_inst_parameter (type));
200215 if (expect_subtype)
201- REQUIRE (type.subtype ()== expect_subtype.value ());
216+ REQUIRE (type.subtype () == expect_subtype.value ());
202217 return type;
203218}
204219
@@ -216,14 +231,11 @@ class_typet require_complete_class(const typet &class_type)
216231 return class_class_type;
217232}
218233
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.
221235// / \param class_type: the class
222- // / \param type_variables: vector of type variables
223236// / \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)
227239{
228240 const class_typet &class_class_type = require_complete_class (class_type);
229241 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(
232244 java_generics_class_typet java_generic_class_type =
233245 to_java_generics_class_type (java_class_type);
234246
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+
251276 return java_generic_class_type;
252277}
253278
0 commit comments