Skip to content

Commit 4033502

Browse files
committed
Add well-formedness check for code_typet
1 parent fb50602 commit 4033502

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

src/util/std_types.h

+15
Original file line numberDiff line numberDiff line change
@@ -981,6 +981,19 @@ class code_typet:public typet
981981
}
982982
return parameter_indices;
983983
}
984+
985+
static void check(
986+
const typet &type,
987+
const validation_modet vm = validation_modet::INVARIANT)
988+
{
989+
DATA_CHECK(
990+
type.find(ID_parameters) != get_nil_irep(),
991+
"code type should indicate parameters");
992+
993+
DATA_CHECK(
994+
type.find(ID_return_type) != get_nil_irep(),
995+
"code type should indicate return type");
996+
}
984997
};
985998

986999
/// Check whether a reference to a typet is a \ref code_typet.
@@ -1003,13 +1016,15 @@ inline bool can_cast_type<code_typet>(const typet &type)
10031016
inline const code_typet &to_code_type(const typet &type)
10041017
{
10051018
PRECONDITION(can_cast_type<code_typet>(type));
1019+
code_typet::check(type);
10061020
return static_cast<const code_typet &>(type);
10071021
}
10081022

10091023
/// \copydoc to_code_type(const typet &)
10101024
inline code_typet &to_code_type(typet &type)
10111025
{
10121026
PRECONDITION(can_cast_type<code_typet>(type));
1027+
code_typet::check(type);
10131028
return static_cast<code_typet &>(type);
10141029
}
10151030

0 commit comments

Comments
 (0)