Skip to content

Commit 232da1d

Browse files
author
thk123
committed
Add can_cast_type for java_generic_typet
Note use is_reference since java_generic_typet inherits from reference_typet so this stronger requirement more closely matches the class hierarchy.
1 parent c1bc380 commit 232da1d

File tree

1 file changed

+9
-7
lines changed

1 file changed

+9
-7
lines changed

jbmc/src/java_bytecode/java_types.h

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -452,31 +452,33 @@ class java_generic_typet:public reference_typet
452452
}
453453
};
454454

455+
template <>
456+
inline bool can_cast_type<java_generic_typet>(const typet &type)
457+
{
458+
return is_reference(type) && type.get_bool(ID_C_java_generic_type);
459+
}
460+
455461
/// \param type: the type to check
456462
/// \return true if type is java type containing with generics, e.g., List<T>
457463
inline bool is_java_generic_type(const typet &type)
458464
{
459-
return type.get_bool(ID_C_java_generic_type);
465+
return can_cast_type<java_generic_typet>(type);
460466
}
461467

462468
/// \param type: source type
463469
/// \return cast of type into java type with generics
464470
inline const java_generic_typet &to_java_generic_type(
465471
const typet &type)
466472
{
467-
PRECONDITION(
468-
type.id()==ID_pointer &&
469-
is_java_generic_type(type));
473+
PRECONDITION(can_cast_type<java_generic_typet>(type));
470474
return static_cast<const java_generic_typet &>(type);
471475
}
472476

473477
/// \param type: source type
474478
/// \return cast of type into java type with generics
475479
inline java_generic_typet &to_java_generic_type(typet &type)
476480
{
477-
PRECONDITION(
478-
type.id()==ID_pointer &&
479-
is_java_generic_type(type));
481+
PRECONDITION(can_cast_type<java_generic_typet>(type));
480482
return static_cast<java_generic_typet &>(type);
481483
}
482484

0 commit comments

Comments
 (0)