Expanding __CPROVER_{r,w,rw}_ok must not introduce overflow [depends-on: #6616]

regression/cbmc/gcc_builtin_add_overflow/conversion-check.c

@@ -0,0 +1,10 @@
+#ifndef __GNUC__
+_Bool __builtin_add_overflow();
+#endif
+
+int main()
+{
+  unsigned a, b, c;
+  if(__builtin_add_overflow(a, b, &c))
+    return 0;
+}

regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc

@@ -0,0 +1,10 @@
+CORE
+conversion-check.c
+--conversion-check --unsigned-overflow-check --signed-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Generated [1-9]\d* VCC\(s\)
+--
+Zero VCCs should be generated.

regression/cbmc/pragma_cprover4/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int nondet_int();
+
+void main()
+{
+  int a = nondet_int();
+  int b = nondet_int();
+  int c = a +
+#pragma CPROVER check disable "signed-overflow"
+          (a + b);
+#pragma CPROVER check pop
+
+#pragma CPROVER check disable "signed-overflow"
+  for(int i = 0; i < 10; ++i)
+  {
+    int temp = a + b;
+#pragma CPROVER check pop
+    int foo = temp + a;
+    assert(foo > 2);
+  }
+}

regression/cbmc/pragma_cprover4/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--signed-overflow-check
+^\[main.overflow.1\] line 9 arithmetic overflow on signed \+ in a \+ a \+ b: FAILURE$
+^\[main.overflow.2\] line 19 arithmetic overflow on signed \+ in temp \+ a: FAILURE$
+^\[main.assertion.1\] line 20 assertion foo > 2: FAILURE$
+^\*\* 3 of 3 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+No assertions other than the above three are expected.

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
+--nan-check _ --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

@@ -1895,6 +1895,33 @@ void goto_check_ct::check_rec_arithmetic_op(
 
 void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
 {
+  flag_overridet resetter(expr.source_location());
+  const auto &pragmas = expr.source_location().get_pragmas();
+  for(const auto &d : pragmas)
+  {
+    // match named-check related pragmas
+    auto matched = match_named_check(d.first);
+    if(matched.has_value())
+    {
+      auto named_check = matched.value();
+      auto name = named_check.first;
+      auto status = named_check.second;
+      bool *flag = name_to_flag.find(name)->second;
+      switch(status)
+      {
+      case check_statust::ENABLE:
+        resetter.set_flag(*flag, true, name);
+        break;
+      case check_statust::DISABLE:
+        resetter.set_flag(*flag, false, name);
+        break;
+      case check_statust::CHECKED:
+        resetter.disable_flag(*flag, name);
+        break;
+      }
+    }
+  }
+
   if(expr.id() == ID_exists || expr.id() == ID_forall)
   {
     // the scoped variables may be used in the assertion
@@ -2020,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)

src/ansi-c/ansi_c_parser.cpp

@@ -203,6 +203,9 @@ void ansi_c_parsert::pragma_cprover_add_check(
 
 bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled)
 {
+  if(pragma_cprover_stack.empty())
+    return false;
+
   auto top = pragma_cprover_stack.back();
   auto found = top.find(name);
   return found != top.end() && found->second != enabled;

src/goto-programs/goto_convert_side_effect.cpp

@@ -656,9 +656,12 @@ void goto_convertt::remove_overflow(
   if(result.type().id() == ID_pointer)
   {
     result_type = to_pointer_type(result.type()).base_type();
-    code_assignt result_assignment{dereference_exprt{result},
-                                   typecast_exprt{operation, *result_type},
-                                   expr.source_location()};
+    source_locationt source_location_annotated = expr.source_location();
+    source_location_annotated.add_pragma("disable:conversion-check");
+    code_assignt result_assignment{
+      dereference_exprt{result},
+      typecast_exprt{operation, *result_type},
+      source_location_annotated};
     convert_assign(result_assignment, dest, mode);
   }
   else