File tree Expand file tree Collapse file tree 1 file changed +23
-0
lines changed Expand file tree Collapse file tree 1 file changed +23
-0
lines changed Original file line number Diff line number Diff line change @@ -1012,6 +1012,29 @@ class object_size_exprt : public unary_exprt
1012
1012
}
1013
1013
};
1014
1014
1015
+ // / \brief Cast an exprt to a \ref object_size_exprt
1016
+ // /
1017
+ // / \a expr must be known to be \ref object_size_exprt.
1018
+ // /
1019
+ // / \param expr: Source expression
1020
+ // / \return Object of type \ref object_size_exprt
1021
+ inline const object_size_exprt &to_object_size_expr (const exprt &expr)
1022
+ {
1023
+ PRECONDITION (expr.id () == ID_object_size);
1024
+ const object_size_exprt &ret = static_cast <const object_size_exprt &>(expr);
1025
+ validate_expr (ret);
1026
+ return ret;
1027
+ }
1028
+
1029
+ // / \copydoc to_object_size_expr(const exprt &)
1030
+ inline object_size_exprt &to_object_size_expr (exprt &expr)
1031
+ {
1032
+ PRECONDITION (expr.id () == ID_object_size);
1033
+ object_size_exprt &ret = static_cast <object_size_exprt &>(expr);
1034
+ validate_expr (ret);
1035
+ return ret;
1036
+ }
1037
+
1015
1038
template <>
1016
1039
inline bool can_cast_expr<object_size_exprt>(const exprt &base)
1017
1040
{
You can’t perform that action at this time.
0 commit comments