Skip to content

Commit d3ff11c

Browse files
author
svorenova
committed
Adding a utility for checking java generic class
1 parent 707ebf6 commit d3ff11c

File tree

2 files changed

+15
-0
lines changed

2 files changed

+15
-0
lines changed

unit/testing-utils/require_type.cpp

+12
Original file line numberDiff line numberDiff 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+
}

unit/testing-utils/require_type.h

+3
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,9 @@ java_generic_parametert require_java_generic_parameter(
6262
const 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

0 commit comments

Comments
 (0)