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
10121012 }
10131013};
10141014
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+
10151038template <>
10161039inline bool can_cast_expr<object_size_exprt>(const exprt &base)
10171040{
You can’t perform that action at this time.
0 commit comments