@@ -78,7 +78,7 @@ code_typet require_type::require_code(
78
78
// / \param function_type: The type of the function
79
79
// / \param param_name: The name of the parameter
80
80
// / \return: A reference to the parameter structure corresponding to this
81
- // / parameter name.
81
+ // / parameter name.
82
82
code_typet::parametert require_type::require_parameter (
83
83
const code_typet &function_type,
84
84
const irep_idt ¶m_name)
@@ -94,104 +94,110 @@ code_typet::parametert require_type::require_parameter(
94
94
return *param;
95
95
}
96
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)
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)
106
105
{
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 )
110
107
{
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 ;
124
116
}
125
-
126
- return generic_type;
117
+ // Should be unreachable...
118
+ REQUIRE (false );
119
+ return false ;
127
120
}
128
121
122
+
129
123
// / 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
+ // /
131
130
// / \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.
134
134
// / \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 (
137
136
const typet &type,
138
- const optionalt<std::initializer_list<irep_idt>> &type_instantiations )
137
+ const optionalt<require_type::expected_type_parameterst> &type_expectations )
139
138
{
140
139
REQUIRE (is_java_generic_type (type));
141
140
const java_generic_typet &generic_type=to_java_generic_type (type);
142
- if (type_instantiations )
141
+ if (type_expectations )
143
142
{
144
143
const java_generic_typet::generic_type_variablest &generic_type_vars=
145
144
generic_type.generic_type_variables ();
146
- REQUIRE (generic_type_vars.size ()==type_instantiations. value (). size ());
145
+ REQUIRE (generic_type_vars.size ()==type_expectations-> size ());
147
146
REQUIRE (
148
147
std::equal (
149
- type_instantiations->begin (),
150
- type_instantiations->end (),
151
148
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));
157
152
}
158
153
159
-
160
154
return generic_type;
161
155
}
162
156
163
157
// / 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
+ // /
165
167
// / \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 (
171
172
const typet &type,
172
- const optionalt<irep_idt > &type_variable )
173
+ const optionalt<require_type::expected_type_parametert > &type_expectation )
173
174
{
174
175
REQUIRE (is_java_generic_parameter (type));
175
176
const java_generic_parametert &generic_param=to_java_generic_parameter (type);
176
- if (type_variable )
177
+ if (type_expectation )
177
178
{
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 () ));
182
183
}
183
184
184
185
return generic_param;
185
186
}
186
187
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
187
193
const typet &require_type::require_java_non_generic_type (
188
194
const typet &type,
189
- const optionalt<irep_idt > &expect_type )
195
+ const optionalt<symbol_typet > &expect_subtype )
190
196
{
191
197
REQUIRE (!is_java_generic_parameter (type));
192
198
REQUIRE (!is_java_generic_type (type));
193
199
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 ());
196
202
return type;
197
203
}
0 commit comments