Test __CPROVER_{r,w}_ok and fix disabled pointer checks

We did not have an explicit test of __CPROVER_{r,w}_ok, only implicit
ones as we use these predicates in our model of the C library. While
preparing a test it became apparent that the predicates are only
evaluated when --pointer-check is set. This caused surprising behaviour
as a negated predicate would result in failing assertions. Instead, make
sure the combined expression always evaluates to true when
--pointer-check is not set.

Author: tautschnig

regression/cbmc/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/cbmc/r_w_ok1/no-check.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^(Starting CEGAR Loop|Generated 10 VCC\(s\), 0 remaining after simplification)$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/r_w_ok1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+__CPROVER_[rw]_ok\(p, n \+ 1\): FAILURE$
+^\*\* 2 of 10 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -118,7 +118,7 @@ class goto_checkt
   void conversion_check(const exprt &, const guardt &);
   void float_overflow_check(const exprt &, const guardt &);
   void nan_check(const exprt &, const guardt &);
-  optionalt<exprt> rw_ok_check(exprt);
+  optionalt<exprt> rw_ok_check(exprt, bool negated);
 
   std::string array_name(const exprt &);
 
@@ -1076,9 +1076,7 @@ void goto_checkt::pointer_validity_check(
 goto_checkt::conditionst
 goto_checkt::address_check(const exprt &address, const exprt &size)
 {
-  if(!enable_pointer_check)
-    return {};
-
+  PRECONDITION(enable_pointer_check);
   PRECONDITION(address.type().id() == ID_pointer);
   const auto &pointer_type = to_pointer_type(address.type());
 
@@ -1654,13 +1652,13 @@ void goto_checkt::check(const exprt &expr)
 }
 
 /// expand the r_ok and w_ok predicates
-optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
+optionalt<exprt> goto_checkt::rw_ok_check(exprt expr, bool negated)
 {
   bool modified = false;
 
   for(auto &op : expr.operands())
   {
-    auto op_result = rw_ok_check(op);
+    auto op_result = rw_ok_check(op, negated != (expr.id() == ID_not));
     if(op_result.has_value())
     {
       op = *op_result;
@@ -1674,6 +1672,14 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
     DATA_INVARIANT(
       expr.operands().size() == 2, "r/w_ok must have two operands");
 
+    if(!enable_pointer_check)
+    {
+      if(negated)
+        return false_exprt{};
+      else
+        return true_exprt{};
+    }
+
     const auto conditions = address_check(expr.op0(), expr.op1());
 
     exprt::operandst conjuncts;
@@ -1844,7 +1850,7 @@ void goto_checkt::goto_check(
     {
       bool is_user_provided=i.source_location.get_bool("user-provided");
 
-      auto rw_ok_cond = rw_ok_check(i.get_condition());
+      auto rw_ok_cond = rw_ok_check(i.get_condition(), false);
       if(rw_ok_cond.has_value())
         i.set_condition(*rw_ok_cond);