Always evaluate __CPROVER_{r,w}_ok and add a test

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 expression is always evaluated, independent of --pointer-check.
This requires always performing a local alias analysis, even when no
pointer checks are enabled.

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/test.desc

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

src/analyses/goto_check.cpp

@@ -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(local_bitvector_analysis);
   PRECONDITION(address.type().id() == ID_pointer);
   const auto &pointer_type = to_pointer_type(address.type());
 
@@ -1700,9 +1698,8 @@ void goto_checkt::goto_check(
 
   bool did_something = false;
 
-  if(enable_pointer_check)
-    local_bitvector_analysis =
-      util_make_unique<local_bitvector_analysist>(goto_function, ns);
+  local_bitvector_analysis =
+    util_make_unique<local_bitvector_analysist>(goto_function, ns);
 
   goto_programt &goto_program=goto_function.body;