Expanding __CPROVER_{r,w,rw}_ok must not introduce overflow

Distributing signed-to-unsigned type casts over addition can result in
an unsigned overflow where previously there was no overflow. That's ok
at the logic level for any expressions yield the same models. We just
need to make sure that expressions generated are not subject to
goto_check_ct generating additional checks: goto_check_ct generates C
language checks, not ones for internally generated expressions.

Author: tautschnig

regression/contracts/simplify-overflow/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  char buf[10];
+  __CPROVER_size_t max = 9;
+  __CPROVER_size_t start = 1;
+
+  __CPROVER_assert(
+    __CPROVER_r_ok(buf + start, max - start), "array is readable");
+}

regression/contracts/simplify-overflow/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+ _ --signed-overflow-check --unsigned-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test doesn't actually use contracts, but rather demonstrates the workflow
+of having goto-instrument expand __CPROVER_r_ok (but really doing nothing else)
+before CBMC when may add (overflow) checks. Doing so must not result in failing
+assertions that would not have failed on the original input.

src/analyses/goto_check_c.cpp

@@ -2047,6 +2047,10 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
     exprt c = conjunction(conjuncts);
     if(enable_simplify)
       simplify(c, ns);
+
+    // this is a logic expression, C language checks no longer apply
+    add_all_disable_named_check_pragmas(c.add_source_location());
+
     return c;
   }
   else if(modified)