__CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end

Author: Daniel Kroening

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