@@ -59,6 +59,21 @@ 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
@@ -78,3 +93,105 @@ code_typet::parametert require_type::require_parameter(
7893 REQUIRE (param != function_type.parameters ().end ());
7994 return *param;
8095}
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)
106+ {
107+ REQUIRE (is_java_generic_type (type));
108+ const java_generic_typet &generic_type=to_java_generic_type (type);
109+ if (type_variables)
110+ {
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+ }));
124+ }
125+
126+ return generic_type;
127+ }
128+
129+ // / Verify a given type is a java_generic_type, optionally checking
130+ // / that it's associated type variables match a given set of identifiers
131+ // / \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.
134+ // / \return The given type, cast to a java_generic_typet
135+ const java_generic_typet
136+ &require_type::require_java_generic_type_instantiations (
137+ const typet &type,
138+ const optionalt<std::initializer_list<irep_idt>> &type_instantiations)
139+ {
140+ REQUIRE (is_java_generic_type (type));
141+ const java_generic_typet &generic_type=to_java_generic_type (type);
142+ if (type_instantiations)
143+ {
144+ const java_generic_typet::generic_type_variablest &generic_type_vars=
145+ generic_type.generic_type_variables ();
146+ REQUIRE (generic_type_vars.size ()==type_instantiations.value ().size ());
147+ REQUIRE (
148+ std::equal (
149+ type_instantiations->begin (),
150+ type_instantiations->end (),
151+ 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+ }));
157+ }
158+
159+
160+ return generic_type;
161+ }
162+
163+ // / Verify a given type is a java_generic_parameter, optionally checking
164+ // / that it's associated type variables match a given set of identifiers
165+ // / \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 (
171+ const typet &type,
172+ const optionalt<irep_idt> &type_variable)
173+ {
174+ REQUIRE (is_java_generic_parameter (type));
175+ const java_generic_parametert &generic_param=to_java_generic_parameter (type);
176+ if (type_variable)
177+ {
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 ());
182+ }
183+
184+ return generic_param;
185+ }
186+
187+ const typet &require_type::require_java_non_generic_type (
188+ const typet &type,
189+ const optionalt<irep_idt> &expect_type)
190+ {
191+ REQUIRE (!is_java_generic_parameter (type));
192+ REQUIRE (!is_java_generic_type (type));
193+ REQUIRE (!is_java_generic_inst_parameter (type));
194+ if (expect_type)
195+ REQUIRE (type.subtype ()==symbol_typet (expect_type.value ()));
196+ return type;
197+ }
0 commit comments