Skip to content

Commit dd86120

Browse files
committed
Add functions to cast to sign_exprt
1 parent 755d839 commit dd86120

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
@@ -696,6 +696,39 @@ class sign_exprt:public unary_predicate_exprt
696696
}
697697
};
698698

699+
/// \brief Cast an exprt to a \ref sign_exprt
700+
///
701+
/// \a expr must be known to be a \ref sign_exprt.
702+
///
703+
/// \param expr: Source expression
704+
/// \return Object of type \ref sign_exprt
705+
inline const sign_exprt &to_sign_expr(const exprt &expr)
706+
{
707+
PRECONDITION(expr.id() == ID_sign);
708+
DATA_INVARIANT(
709+
expr.operands().size() == 1, "sign expression must have one operand");
710+
return static_cast<const sign_exprt &>(expr);
711+
}
712+
713+
/// \copydoc to_sign_expr(const exprt &)
714+
inline sign_exprt &to_sign_expr(exprt &expr)
715+
{
716+
PRECONDITION(expr.id() == ID_sign);
717+
DATA_INVARIANT(
718+
expr.operands().size() == 1, "sign expression must have one operand");
719+
return static_cast<sign_exprt &>(expr);
720+
}
721+
722+
template <>
723+
inline bool can_cast_expr<sign_exprt>(const exprt &base)
724+
{
725+
return base.id() == ID_sign;
726+
}
727+
inline void validate_expr(const sign_exprt &expr)
728+
{
729+
validate_operands(expr, 1, "sign expression must have one operand");
730+
}
731+
699732
/// \brief A base class for binary expressions
700733
class binary_exprt:public exprt
701734
{

0 commit comments

Comments
 (0)