fix writeset inclusion checks on DEAD instructions

When handling DEAD instructions in function/loop assigns clause
instrumentation, the instruction iterator was not being incremented
correctly.
This led to instrumentation outside of the function/loop scope, and
spurious write set inclusion violations.

Moreover, for loops, declarations of some temporaries (those involved in
the "initialization" of loop counter, for instance) are "outside" of the
loop identified by CBMC, so we no longer raise an exception on not
finding a corresponding DECL for each DEAD.
These variables are writable because they appear as assigns clause
targets, not because they were local DECLs.

Author: SaswatPadhi

regression/contracts/loop_assigns-05/main.c

@@ -0,0 +1,59 @@
+#include <assert.h>
+
+int j;
+
+int lowerbound()
+{
+  return 0;
+}
+
+int upperbound()
+{
+  return 10;
+}
+
+void incr(int *i)
+{
+  (*i)++;
+}
+
+void body_1(int i)
+{
+  j = i;
+}
+
+void body_2(int *i)
+{
+  (*i)++;
+  (*i)--;
+}
+
+int body_3(int *i)
+{
+  (*i)++;
+  if(*i == 4)
+    return 1;
+
+  (*i)--;
+  return 0;
+}
+
+int main()
+{
+  for(int i = lowerbound(); i < upperbound(); incr(&i))
+    // clang-format off
+    __CPROVER_assigns(i, j)
+    __CPROVER_loop_invariant(0 <= i && i <= 10)
+    __CPROVER_loop_invariant(i != 0 ==> j + 1 == i)
+    // clang-format on
+    {
+      body_1(i);
+
+      if(body_3(&i))
+        return 1;
+
+      body_2(&i);
+    }
+
+  assert(j == 9);
+}

regression/contracts/loop_assigns-05/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[body_1.\d+\] .* Check that j is assignable: SUCCESS$
+^\[body_2.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[body_3.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[incr.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks write set inclusion checks in presence of function calls,
+which are inlined, and also checks that DEAD instructions introduced during
+inlining is correctly handled.

src/goto-instrument/contracts/contracts.cpp

@@ -1054,20 +1054,28 @@ void code_contractst::check_frame_conditions(
         assigns_clauset::conditional_address_ranget{assigns, symbol});
       if(symbol_car != assigns.get_write_set().end())
       {
-        instruction_it++;
         auto invalidation_assignment = goto_programt::make_assignment(
           symbol_car->validity_condition_var,
           false_exprt{},
           instruction_it->source_location());
-        // note that instruction_it is not advanced by this call,
-        // so no need to move it backwards
-        body.insert_before_swap(instruction_it, invalidation_assignment);
+        // note that the CAR must be invalidated _after_ the DEAD instruction
+        body.insert_after(
+          instruction_it,
+          add_pragma_disable_assigns_check(invalidation_assignment));
       }
       else
       {
-        throw incorrect_goto_program_exceptiont(
-          "Found a `DEAD` variable without corresponding `DECL`!",
-          instruction_it->source_location());
+        // For loops, the loop_head appears after the DECL of counters,
+        // and any other temporaries introduced during "initialization".
+        // However, they go `DEAD` (possible conditionally) inside the loop,
+        // in presence of return statements.
+        // Notice that for them those variables be writable,
+        // they must appear as assigns targets anyway,
+        // but their DECL statements are outside of the loop.
+        log.warning() << "Found a `DEAD` variable "
+                      << name2string(symbol.get_identifier())
+                      << " without corresponding `DECL`, at: "
+                      << instruction_it->source_location() << messaget::eom;
       }
     }
     else if(