@@ -59,11 +59,26 @@ code_typet require_type::require_code(const typet &type)
5959 return to_code_type (type);
6060}
6161
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+
6277// / Verify that a function has a parameter of a specific name.
6378// / \param function_type: The type of the function
6479// / \param param_name: The name of the parameter
6580// / \return: A reference to the parameter structure corresponding to this
66- // / parameter name.
81+ // / parameter name.
6782code_typet::parametert require_type::require_parameter (
6883 const code_typet &function_type,
6984 const irep_idt ¶m_name)
@@ -78,3 +93,111 @@ code_typet::parametert require_type::require_parameter(
7893 REQUIRE (param != function_type.parameters ().end ());
7994 return *param;
8095}
96+
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)
105+ {
106+ switch (expected.kind )
107+ {
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 ;
116+ }
117+ // Should be unreachable...
118+ REQUIRE (false );
119+ return false ;
120+ }
121+
122+
123+ // / Verify a given type is a java_generic_type, optionally checking
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+ // /
130+ // / \param type The type to check
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+ // / \return The given type, cast to a java_generic_typet
135+ java_generic_typet require_type::require_java_generic_type (
136+ const typet &type,
137+ const optionalt<require_type::expected_type_parameterst> &type_expectations)
138+ {
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+ }
153+
154+ return generic_type;
155+ }
156+
157+ // / Verify a given type is a java_generic_parameter, optionally checking
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+ // /
167+ // / \param type The type to check
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 (
172+ const typet &type,
173+ const optionalt<require_type::expected_type_parametert> &type_expectation)
174+ {
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+ }
184+
185+ return generic_param;
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
193+ const typet &require_type::require_java_non_generic_type (
194+ const typet &type,
195+ const optionalt<symbol_typet> &expect_subtype)
196+ {
197+ REQUIRE (!is_java_generic_parameter (type));
198+ REQUIRE (!is_java_generic_type (type));
199+ REQUIRE (!is_java_generic_inst_parameter (type));
200+ if (expect_subtype)
201+ REQUIRE (type.subtype ()==expect_subtype.value ());
202+ return type;
203+ }
0 commit comments