Skip to content

Commit dcb925a

Browse files
committed
Add functions to cast to sign_exprt
1 parent 13360bf commit dcb925a

File tree

1 file changed

+33
-0
lines changed

1 file changed

+33
-0
lines changed

src/util/std_expr.h

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -615,6 +615,39 @@ class sign_exprt:public unary_predicate_exprt
615615
}
616616
};
617617

618+
/// \brief Cast an exprt to a \ref sign_exprt
619+
///
620+
/// \a expr must be known to be a \ref sign_exprt.
621+
///
622+
/// \param expr: Source expression
623+
/// \return Object of type \ref sign_exprt
624+
inline const sign_exprt &to_sign_expr(const exprt &expr)
625+
{
626+
PRECONDITION(expr.id() == ID_sign);
627+
DATA_INVARIANT(
628+
expr.operands().size() == 1, "sign expression must have one operand");
629+
return static_cast<const sign_exprt &>(expr);
630+
}
631+
632+
/// \copydoc to_sign_expr(const exprt &)
633+
inline sign_exprt &to_sign_expr(exprt &expr)
634+
{
635+
PRECONDITION(expr.id() == ID_sign);
636+
DATA_INVARIANT(
637+
expr.operands().size() == 1, "sign expression must have one operand");
638+
return static_cast<sign_exprt &>(expr);
639+
}
640+
641+
template <>
642+
inline bool can_cast_expr<sign_exprt>(const exprt &base)
643+
{
644+
return base.id() == ID_sign;
645+
}
646+
inline void validate_expr(const sign_exprt &expr)
647+
{
648+
validate_operands(expr, 1, "sign expression must have one operand");
649+
}
650+
618651
/// \brief A base class for binary expressions
619652
class binary_exprt:public exprt
620653
{

0 commit comments

Comments
 (0)