Merge pull request #7560 from tautschnig/bugfixes/r_w_ok-decl

Avoid confusing "__CPROVER_{r,w,rw}_ok is not declared" warning

Author: kroening

regression/ansi-c/r_w_ok-expected-failures/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int *p = (int *)0;
+#ifdef TOO_MANY_ARGS
+  assert(!__CPROVER_r_ok(p, sizeof(int), 42));
+#elif defined(NOT_A_POINTER)
+  assert(!__CPROVER_r_ok(*p, sizeof(int)));
+#elif defined(VOID_POINTER_NO_SIZE)
+  assert(!__CPROVER_r_ok((void *)p));
+#endif
+}

regression/ansi-c/r_w_ok-expected-failures/not_a_pointer.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+-DNOT_A_POINTER
+__CPROVER_r_ok expects a pointer as first argument$
+^CONVERSION ERROR$
+^EXIT=(64|1)$
+^SIGNAL=0$

regression/ansi-c/r_w_ok-expected-failures/too_many_arguments.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+-DTOO_MANY_ARGS
+__CPROVER_r_ok expects one or two operands$
+^CONVERSION ERROR$
+^EXIT=(64|1)$
+^SIGNAL=0$

regression/ansi-c/r_w_ok-expected-failures/void_pointer_no_size.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+-DVOID_POINTER_NO_SIZE
+__CPROVER_r_ok expects a size when given a void pointer$
+^CONVERSION ERROR$
+^EXIT=(64|1)$
+^SIGNAL=0$

regression/ansi-c/r_w_ok1/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p = NULL;
+
+  assert(!__CPROVER_r_ok(p, sizeof(int)));
+  assert(!__CPROVER_w_ok(p, sizeof(int)));
+
+  p = malloc(sizeof(int));
+
+  assert(__CPROVER_r_ok(p, 1));
+  assert(__CPROVER_w_ok(p, 1));
+  assert(__CPROVER_r_ok(p, sizeof(int)));
+  assert(__CPROVER_w_ok(p, sizeof(int)));
+
+  size_t n;
+  char *arbitrary_size = malloc(n);
+
+  assert(__CPROVER_r_ok(arbitrary_size, n));
+  assert(__CPROVER_w_ok(arbitrary_size, n));
+
+  assert(__CPROVER_r_ok(arbitrary_size, n + 1));
+  assert(__CPROVER_w_ok(arbitrary_size, n + 1));
+}

regression/ansi-c/r_w_ok1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verbosity 2
+^EXIT=0$
+^SIGNAL=0$
+--
+function '__CPROVER_[rw]_ok' is not declared

src/ansi-c/c_typecheck_expr.cpp

@@ -2218,6 +2218,70 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
         expr.swap(lowered);
         return;
       }
+      else if(
+        identifier == CPROVER_PREFIX "r_ok" ||
+        identifier == CPROVER_PREFIX "w_ok" ||
+        identifier == CPROVER_PREFIX "rw_ok")
+      {
+        if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
+        {
+          throw invalid_source_file_exceptiont{
+            id2string(identifier) + " expects one or two operands",
+            f_op.source_location()};
+        }
+
+        // the first argument must be a pointer
+        auto &pointer_expr = expr.arguments()[0];
+        if(pointer_expr.type().id() == ID_array)
+        {
+          auto dest_type = pointer_type(void_type());
+          dest_type.base_type().set(ID_C_constant, true);
+          implicit_typecast(pointer_expr, dest_type);
+        }
+        else if(pointer_expr.type().id() != ID_pointer)
+        {
+          throw invalid_source_file_exceptiont{
+            id2string(identifier) + " expects a pointer as first argument",
+            f_op.source_location()};
+        }
+
+        // The second argument, when given, is a size_t.
+        // When not given, use the pointer subtype.
+        exprt size_expr;
+
+        if(expr.arguments().size() == 2)
+        {
+          implicit_typecast(expr.arguments()[1], size_type());
+          size_expr = expr.arguments()[1];
+        }
+        else
+        {
+          // Won't do void *
+          const auto &subtype =
+            to_pointer_type(pointer_expr.type()).base_type();
+          if(subtype.id() == ID_empty)
+          {
+            throw invalid_source_file_exceptiont{
+              id2string(identifier) +
+                " expects a size when given a void pointer",
+              f_op.source_location()};
+          }
+
+          auto size_expr_opt = size_of_expr(subtype, *this);
+          CHECK_RETURN(size_expr_opt.has_value());
+          size_expr = std::move(size_expr_opt.value());
+        }
+
+        irep_idt id = identifier == CPROVER_PREFIX "r_ok"   ? ID_r_ok
+                      : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok
+                                                            : ID_rw_ok;
+
+        r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
+        ok_expr.add_source_location() = expr.source_location();
+
+        expr.swap(ok_expr);
+        return;
+      }
       else if(
         auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
           identifier, expr.arguments(), f_op.source_location()))
@@ -3145,70 +3209,6 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(malloc_expr);
   }
-  else if(
-    identifier == CPROVER_PREFIX "r_ok" ||
-    identifier == CPROVER_PREFIX "w_ok" || identifier == CPROVER_PREFIX "rw_ok")
-  {
-    if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
-    {
-      error().source_location = f_op.source_location();
-      error() << identifier << " expects one or two operands" << eom;
-      throw 0;
-    }
-
-    typecheck_function_call_arguments(expr);
-
-    // the first argument must be a pointer
-    const auto &pointer_expr = expr.arguments()[0];
-    if(pointer_expr.type().id() != ID_pointer)
-    {
-      error().source_location = f_op.source_location();
-      error() << identifier << " expects a pointer as first argument" << eom;
-      throw 0;
-    }
-
-    // The second argument, when given, is a size_t.
-    // When not given, use the pointer subtype.
-    exprt size_expr;
-
-    if(expr.arguments().size() == 2)
-    {
-      implicit_typecast(expr.arguments()[1], size_type());
-      size_expr = expr.arguments()[1];
-    }
-    else
-    {
-      // Won't do void *
-      const auto &subtype = to_pointer_type(pointer_expr.type()).base_type();
-      if(subtype.id() == ID_empty)
-      {
-        error().source_location = f_op.source_location();
-        error() << identifier << " expects a size when given a void pointer"
-                << eom;
-        throw 0;
-      }
-
-      auto size_expr_opt = size_of_expr(subtype, *this);
-      if(!size_expr_opt.has_value())
-      {
-        error().source_location = f_op.source_location();
-        error() << identifier << " was given object pointer without size"
-                << eom;
-        throw 0;
-      }
-
-      size_expr = std::move(size_expr_opt.value());
-    }
-
-    irep_idt id = identifier == CPROVER_PREFIX "r_ok"
-                    ? ID_r_ok
-                    : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok : ID_rw_ok;
-
-    r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
-    ok_expr.add_source_location() = source_location;
-
-    return std::move(ok_expr);
-  }
   else if(
     (identifier == CPROVER_PREFIX "old") ||
     (identifier == CPROVER_PREFIX "loop_entry"))