Skip to content

Commit 4040cc0

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 ef93335 commit 4040cc0

File tree

1 file changed

+10
-7
lines changed

1 file changed

+10
-7
lines changed

jbmc/src/java_bytecode/java_types.h

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -452,31 +452,34 @@ 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) &&
459+
type.get_bool(ID_C_java_generic_type);
460+
}
461+
455462
/// \param type: the type to check
456463
/// \return true if type is java type containing with generics, e.g., List<T>
457464
inline bool is_java_generic_type(const typet &type)
458465
{
459-
return type.get_bool(ID_C_java_generic_type);
466+
return can_cast_type<java_generic_typet>(type);
460467
}
461468

462469
/// \param type: source type
463470
/// \return cast of type into java type with generics
464471
inline const java_generic_typet &to_java_generic_type(
465472
const typet &type)
466473
{
467-
PRECONDITION(
468-
type.id()==ID_pointer &&
469-
is_java_generic_type(type));
474+
PRECONDITION(can_cast_type<java_generic_typet>(type));
470475
return static_cast<const java_generic_typet &>(type);
471476
}
472477

473478
/// \param type: source type
474479
/// \return cast of type into java type with generics
475480
inline java_generic_typet &to_java_generic_type(typet &type)
476481
{
477-
PRECONDITION(
478-
type.id()==ID_pointer &&
479-
is_java_generic_type(type));
482+
PRECONDITION(can_cast_type<java_generic_typet>(type));
480483
return static_cast<java_generic_typet &>(type);
481484
}
482485

0 commit comments

Comments
 (0)