Merge pull request #7461 from tautschnig/cleanup/rw_ok-cast

r/w/rw_ok: implement can_cast_expr and validate_expr

Author: kroening

src/util/pointer_expr.h

@@ -818,6 +818,17 @@ class r_or_w_ok_exprt : public binary_predicate_exprt
   }
 };
 
+template <>
+inline bool can_cast_expr<r_or_w_ok_exprt>(const exprt &base)
+{
+  return base.id() == ID_r_ok || base.id() == ID_w_ok || base.id() == ID_rw_ok;
+}
+
+inline void validate_expr(const r_or_w_ok_exprt &value)
+{
+  validate_operands(value, 2, "r_or_w_ok must have two operands");
+}
+
 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
 {
   PRECONDITION(
@@ -837,6 +848,17 @@ class r_ok_exprt : public r_or_w_ok_exprt
   }
 };
 
+template <>
+inline bool can_cast_expr<r_ok_exprt>(const exprt &base)
+{
+  return base.id() == ID_r_ok;
+}
+
+inline void validate_expr(const r_ok_exprt &value)
+{
+  validate_operands(value, 2, "r_ok must have two operands");
+}
+
 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_r_ok);
@@ -855,6 +877,17 @@ class w_ok_exprt : public r_or_w_ok_exprt
   }
 };
 
+template <>
+inline bool can_cast_expr<w_ok_exprt>(const exprt &base)
+{
+  return base.id() == ID_w_ok;
+}
+
+inline void validate_expr(const w_ok_exprt &value)
+{
+  validate_operands(value, 2, "w_ok must have two operands");
+}
+
 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_w_ok);