Merge pull request #7125 from diffblue/writeable_object

writeable_object and live_object

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -2498,6 +2498,38 @@ exprt c_typecheck_baset::do_special_functions(
 
     return is_dynamic_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "LIVE_OBJECT")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "live_object expects one argument" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt live_object_expr = live_object_exprt(expr.arguments()[0]);
+    live_object_expr.add_source_location() = source_location;
+
+    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,8 @@ void __CPROVER_old(const void *);
 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

@@ -3988,6 +3988,8 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_count_leading_zeros, "__builtin_clz"},
     {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*"},