@@ -78,7 +78,7 @@ code_typet require_type::require_code(
7878// / \param function_type: The type of the function
7979// / \param param_name: The name of the parameter
8080// / \return: A reference to the parameter structure corresponding to this
81- // / parameter name.
81+ // / parameter name.
8282code_typet::parametert require_type::require_parameter (
8383 const code_typet &function_type,
8484 const irep_idt ¶m_name)
@@ -94,104 +94,110 @@ code_typet::parametert require_type::require_parameter(
9494 return *param;
9595}
9696
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)
97+ // / Helper function for testing that java_generic_parametert types match
98+ // / a given expectation.
99+ // / \param param The generic parameter to test
100+ // / \param expected The expected value of the parameter
101+ // / \return true if the generic parameter type meets the expectations
102+ bool require_java_generic_parametert_expectation (
103+ const java_generic_parametert ¶m,
104+ const require_type::expected_type_parametert &expected)
106105{
107- REQUIRE (is_java_generic_type (type));
108- const java_generic_typet &generic_type=to_java_generic_type (type);
109- if (type_variables)
106+ switch (expected.kind )
110107 {
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- }));
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 ;
124116 }
125-
126- return generic_type;
117+ // Should be unreachable...
118+ REQUIRE (false );
119+ return false ;
127120}
128121
122+
129123// / Verify a given type is a java_generic_type, optionally checking
130- // / that it's associated type variables match a given set of identifiers
124+ // / that it's associated type variables match a given set of identifiers.
125+ // / Expected usage is something like this:
126+ // /
127+ // / require_java_generic_type(type,
128+ // / {{Inst,"java::java.lang.Integer"},{Var,"T"}})
129+ // /
131130// / \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.
131+ // / \param type_expectations An optional set of type variable kinds
132+ // / and identifiers which should be expected as the type parameters of the
133+ // / given generic type.
134134// / \return The given type, cast to a java_generic_typet
135- const java_generic_typet
136- &require_type::require_java_generic_type_instantiations (
135+ java_generic_typet require_type::require_java_generic_type (
137136 const typet &type,
138- const optionalt<std::initializer_list<irep_idt>> &type_instantiations )
137+ const optionalt<require_type::expected_type_parameterst> &type_expectations )
139138{
140139 REQUIRE (is_java_generic_type (type));
141140 const java_generic_typet &generic_type=to_java_generic_type (type);
142- if (type_instantiations )
141+ if (type_expectations )
143142 {
144143 const java_generic_typet::generic_type_variablest &generic_type_vars=
145144 generic_type.generic_type_variables ();
146- REQUIRE (generic_type_vars.size ()==type_instantiations. value (). size ());
145+ REQUIRE (generic_type_vars.size ()==type_expectations-> size ());
147146 REQUIRE (
148147 std::equal (
149- type_instantiations->begin (),
150- type_instantiations->end (),
151148 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- }));
149+ generic_type_vars.end (),
150+ type_expectations->begin (),
151+ require_java_generic_parametert_expectation));
157152 }
158153
159-
160154 return generic_type;
161155}
162156
163157// / Verify a given type is a java_generic_parameter, optionally checking
164- // / that it's associated type variables match a given set of identifiers
158+ // / that it's associated type variables match a given set of expectations.
159+ // / Expected usage is something like this:
160+ // /
161+ // / require_java_generic_parameter(parameter, {Inst,"java::java.lang.Integer"})
162+ // /
163+ // / or
164+ // /
165+ // / require_java_generic_parameter(parameter, {Var,"T"})
166+ // /
165167// / \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 (
168+ // / \param type_expectation An optional description of the identifiers/kinds
169+ // / which / should be expected as the type parameter of the generic parameter.
170+ // / \return The given type, cast to a java_generic_parametert
171+ java_generic_parametert require_type::require_java_generic_parameter (
171172 const typet &type,
172- const optionalt<irep_idt > &type_variable )
173+ const optionalt<require_type::expected_type_parametert > &type_expectation )
173174{
174175 REQUIRE (is_java_generic_parameter (type));
175176 const java_generic_parametert &generic_param=to_java_generic_parameter (type);
176- if (type_variable )
177+ if (type_expectation )
177178 {
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 ());
179+ REQUIRE (
180+ require_java_generic_parametert_expectation (
181+ generic_param,
182+ type_expectation. value () ));
182183 }
183184
184185 return generic_param;
185186}
186187
188+ // / Test a type to ensure it is not a java generics type.
189+ // / \param type The type to test
190+ // / \param expect_subtype Optionally, also test that the subtype of the given
191+ // / type matches this parameter
192+ // / \return The value passed in the first argument
187193const typet &require_type::require_java_non_generic_type (
188194 const typet &type,
189- const optionalt<irep_idt > &expect_type )
195+ const optionalt<symbol_typet > &expect_subtype )
190196{
191197 REQUIRE (!is_java_generic_parameter (type));
192198 REQUIRE (!is_java_generic_type (type));
193199 REQUIRE (!is_java_generic_inst_parameter (type));
194- if (expect_type )
195- REQUIRE (type.subtype ()==symbol_typet (expect_type .value () ));
200+ if (expect_subtype )
201+ REQUIRE (type.subtype ()==expect_subtype .value ());
196202 return type;
197203}
0 commit comments