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
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -1718,8 +1718,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());
+        if(rw_ok_cond.has_value())
+          i.set_condition(*rw_ok_cond);
+      }
+    }
+
     // magic ERROR label?
     for(const auto &label : error_labels)
     {
@@ -1762,6 +1773,16 @@ void goto_checkt::goto_check(
 
       // the LHS might invalidate any assertion
       invalidate(code_assign.lhs());
+
+      if(has_subexpr(code_assign.rhs(), [](const exprt &expr) {
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+         }))
+      {
+        exprt &rhs = to_code_assign(i.code).rhs();
+        auto rw_ok_cond = rw_ok_check(rhs);
+        if(rw_ok_cond.has_value())
+          rhs = *rw_ok_cond;
+      }
     }
     else if(i.is_function_call())
     {
@@ -1810,6 +1831,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());
+          if(rw_ok_cond.has_value())
+            i.code.op0() = *rw_ok_cond;
+        }
       }
     }
     else if(i.is_throw())
@@ -1841,10 +1871,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());
-      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))