introduce __CPROVER_WRITEABLE_OBJECT

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2508,6 +2508,22 @@ exprt c_typecheck_baset::do_special_functions(
 
     return live_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "writeable_object expects one argument" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt writeable_object_expr = writeable_object_exprt(expr.arguments()[0]);
+    writeable_object_expr.add_source_location() = source_location;
+
+    return writeable_object_expr;
+  }
   else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -49,6 +49,7 @@ void __CPROVER_loop_entry(const void *);
 
 // pointers
 __CPROVER_bool __CPROVER_LIVE_OBJECT(const void *);
+__CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *);
 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);

src/ansi-c/expr2c.cpp

@@ -3994,6 +3994,7 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_count_trailing_zeros, "__builtin_ctz"},
     {ID_dynamic_object, "DYNAMIC_OBJECT"},
     {ID_live_object, "LIVE_OBJECT"},
+    {ID_writeable_object, "WRITEABLE_OBJECT"},
     {ID_floatbv_div, "FLOAT/"},
     {ID_floatbv_minus, "FLOAT-"},
     {ID_floatbv_mult, "FLOAT*"},

src/util/irep_ids.def

@@ -454,6 +454,7 @@ IREP_ID_ONE(is_dynamic_object)
 IREP_ID_ONE(dynamic_object)
 IREP_ID_TWO(C_dynamic, #dynamic)
 IREP_ID_ONE(live_object)
+IREP_ID_ONE(writeable_object)
 IREP_ID_ONE(object_size)
 IREP_ID_ONE(good_pointer)
 IREP_ID_ONE(integer_address)

src/util/pointer_expr.h

@@ -1118,4 +1118,58 @@ inline live_object_exprt &to_live_object_expr(exprt &expr)
   return ret;
 }
 
+/// A predicate that indicates that the object pointed to is writeable
+class writeable_object_exprt : public unary_predicate_exprt
+{
+public:
+  explicit writeable_object_exprt(exprt pointer)
+    : unary_predicate_exprt(ID_writeable_object, std::move(pointer))
+  {
+  }
+
+  exprt &pointer()
+  {
+    return op0();
+  }
+
+  const exprt &pointer() const
+  {
+    return op0();
+  }
+};
+
+template <>
+inline bool can_cast_expr<writeable_object_exprt>(const exprt &base)
+{
+  return base.id() == ID_writeable_object;
+}
+
+inline void validate_expr(const writeable_object_exprt &value)
+{
+  validate_operands(value, 1, "writeable_object must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref writeable_object_exprt
+///
+/// \a expr must be known to be \ref writeable_object_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref writeable_object_exprt
+inline const writeable_object_exprt &to_writeable_object_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_writeable_object);
+  const writeable_object_exprt &ret = static_cast<const writeable_object_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_writeable_object_expr(const exprt &)
+inline writeable_object_exprt &to_writeable_object_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_writeable_object);
+  writeable_object_exprt &ret = static_cast<writeable_object_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H