__CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end

Author: Daniel Kroening

doc/cbmc-user-manual.md

@@ -2190,6 +2190,15 @@ to the program. If the expression evaluates to false, the execution
 aborts without failure. More detail on the use of assumptions is in the
 section on [Assumptions and Assertions](modeling-assertions.shtml).
 
+#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
+
+    void __CPROVER_r_ok(const void *, size_t size);
+    void __CPROVER_w_ok(cosnt void *, size_t size);
+
+The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
+memory starting at the given pointer with the given size is safe.
+**\_\_CPROVER\_w_ok** does the same with writing.
+
 #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
 
     _Bool __CPROVER_same_object(const void *, const void *);

src/ansi-c/c_typecheck_expr.cpp

@@ -2334,6 +2334,23 @@ exprt c_typecheck_baset::do_special_functions(
 
     return malloc_expr;
   }
+  else if(
+    identifier == CPROVER_PREFIX "r_ok" || identifier == CPROVER_PREFIX "w_ok")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      err_location(f_op);
+      error() << identifier << " expects two operands" << eom;
+      throw 0;
+    }
+
+    irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
+
+    predicate_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]);
+    ok_expr.add_source_location() = source_location;
+
+    return ok_expr;
+  }
   else if(identifier==CPROVER_PREFIX "isinff" ||
           identifier==CPROVER_PREFIX "isinfd" ||
           identifier==CPROVER_PREFIX "isinfld" ||

src/ansi-c/cprover_builtin_headers.h

@@ -9,6 +9,8 @@ __CPROVER_bool __CPROVER_invalid_pointer(const void *);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
+__CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
 
 // bitvector analysis
 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);

src/ansi-c/expr2c.cpp

@@ -3515,6 +3515,12 @@ std::string expr2ct::convert_with_precedence(
       return convert_function(src, "__builtin_popcount", precedence=16);
   }
 
+  else if(src.id() == ID_r_ok)
+    return convert_function(src, "R_OK", precedence = 16);
+
+  else if(src.id() == ID_w_ok)
+    return convert_function(src, "W_OK", precedence = 16);
+
   else if(src.id()==ID_invalid_pointer)
     return convert_function(src, "INVALID-POINTER", precedence=16);
 

src/ansi-c/library/cprover.h

@@ -24,6 +24,8 @@ void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
+__CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
 
 #if 0
 __CPROVER_bool __CPROVER_equal();

src/util/irep_ids.def

@@ -691,6 +691,8 @@ IREP_ID_TWO(C_unnamed_object, #unnamed_object)
 IREP_ID_TWO(C_temporary_avoided, #temporary_avoided)
 IREP_ID_TWO(C_qualifier, #qualifier)
 IREP_ID_TWO(C_array_ini, #array_ini)
+IREP_ID_ONE(r_ok)
+IREP_ID_ONE(w_ok)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree