Support __CPROVER_{r,w}_ok in assignments, assumptions, gotos, returns

We previously only evaluated __CPROVER_{r,w}_ok in assertions (without
telling anyone that was the case). Instead, evaluate it in all contexts
where it might reasonably appear.

Author: tautschnig

regression/cbmc/r_w_ok2/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int *p = (int *)0;
+
+  _Bool not_ok = !__CPROVER_r_ok(p, sizeof(int));
+  assert(not_ok);
+
+  if(__CPROVER_w_ok(p, sizeof(int)))
+    assert(0);
+}

regression/cbmc/r_w_ok2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -1727,8 +1727,19 @@ void goto_checkt::goto_check(
       assertions.clear();
 
     if(i.has_condition())
+    {
       check(i.get_condition());
 
+      if(has_subexpr(i.get_condition(), [](const exprt &expr) {
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+         }))
+      {
+        auto rw_ok_cond = rw_ok_check(i.get_condition(), false);
+        if(rw_ok_cond.has_value())
+          i.set_condition(*rw_ok_cond);
+      }
+    }
+
     // magic ERROR label?
     for(const auto &label : error_labels)
     {
@@ -1771,6 +1782,15 @@ void goto_checkt::goto_check(
 
       // the LHS might invalidate any assertion
       invalidate(code_assign.lhs());
+
+      if(has_subexpr(i.code.op1(), [](const exprt &expr) {
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+         }))
+      {
+        auto rw_ok_cond = rw_ok_check(i.code.op1(), false);
+        if(rw_ok_cond.has_value())
+          i.code.op1() = *rw_ok_cond;
+      }
     }
     else if(i.is_function_call())
     {
@@ -1819,6 +1839,15 @@ void goto_checkt::goto_check(
         check(i.code.op0());
         // the return value invalidate any assertion
         invalidate(i.code.op0());
+
+        if(has_subexpr(i.code.op0(), [](const exprt &expr) {
+             return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+           }))
+        {
+          auto rw_ok_cond = rw_ok_check(i.code.op0(), false);
+          if(rw_ok_cond.has_value())
+            i.code.op0() = *rw_ok_cond;
+        }
       }
     }
     else if(i.is_throw())
@@ -1850,10 +1879,6 @@ 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(), false);
-      if(rw_ok_cond.has_value())
-        i.set_condition(*rw_ok_cond);
-
       if((is_user_provided && !enable_assertions &&
           i.source_location.get_property_class()!="error label") ||
          (!is_user_provided && !enable_built_in_assertions))