File tree Expand file tree Collapse file tree 2 files changed +15
-0
lines changed Expand file tree Collapse file tree 2 files changed +15
-0
lines changed Original file line number Diff line number Diff line change @@ -201,3 +201,15 @@ const typet &require_type::require_java_non_generic_type(
201201 REQUIRE (type.subtype ()==expect_subtype.value ());
202202 return type;
203203}
204+
205+ // / Verify that a class is a valid java generic class
206+ // / \param class_type: the class
207+ // / \return: A reference to the java generic class type.
208+ java_generics_class_typet &
209+ require_type::require_java_generic_class (const class_typet &class_type)
210+ {
211+ java_class_typet java_class_type = to_java_class_type (class_type);
212+
213+ REQUIRE (is_java_generics_class_type (java_class_type));
214+ return to_java_generics_class_type (java_class_type);
215+ }
Original file line number Diff line number Diff line change @@ -62,6 +62,9 @@ java_generic_parametert require_java_generic_parameter(
6262const typet &require_java_non_generic_type (
6363 const typet &type,
6464 const optionalt<symbol_typet> &expect_subtype);
65+
66+ java_generics_class_typet &
67+ require_java_generic_class (const class_typet &class_type);
6568}
6669
6770#endif // CPROVER_TESTING_UTILS_REQUIRE_TYPE_H
You can’t perform that action at this time.
0 commit comments