introduce is_cstring_exprt

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2411,8 +2411,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    predicate_exprt is_cstring_expr("is_cstring");
-    is_cstring_expr.operands()=expr.arguments();
+    is_cstring_exprt is_cstring_expr(expr.arguments()[0]);
     is_cstring_expr.add_source_location()=source_location;
 
     return std::move(is_cstring_expr);

src/util/pointer_expr.h

@@ -1276,4 +1276,60 @@ inline separate_exprt &to_separate_expr(exprt &expr)
   return ret;
 }
 
+/// A predicate that indicates that a zero-terminated string
+/// starts at the given address
+class is_cstring_exprt : public unary_predicate_exprt
+{
+public:
+  explicit is_cstring_exprt(exprt address)
+    : unary_predicate_exprt(ID_is_cstring, std::move(address))
+  {
+    PRECONDITION(this->address().type().id() == ID_pointer);
+  }
+
+  exprt &address()
+  {
+    return op0();
+  }
+
+  const exprt &address() const
+  {
+    return op0();
+  }
+};
+
+template <>
+inline bool can_cast_expr<is_cstring_exprt>(const exprt &base)
+{
+  return base.id() == ID_is_cstring;
+}
+
+inline void validate_expr(const is_cstring_exprt &value)
+{
+  validate_operands(value, 1, "is_cstring must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref is_cstring_exprt
+///
+/// \a expr must be known to be \ref is_cstring_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref is_cstring_exprt
+inline const is_cstring_exprt &to_is_cstring_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_is_cstring);
+  const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_is_cstring_expr(const exprt &)
+inline is_cstring_exprt &to_is_cstring_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_is_cstring);
+  is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H