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.

Author: SaswatPadhi

regression/contracts/loop_assigns-05/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+
+int j;
+
+int lowerbound()
+{
+  return 0;
+}
+
+int upperbound()
+{
+  return 10;
+}
+
+void incr(int *i)
+{
+  (*i)++;
+}
+
+void body(int i)
+{
+  j = i;
+}
+
+void 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(i);
+    }
+
+  assert(j == 9);
+}

regression/contracts/loop_assigns-05/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[body.\d+\] .* Check that j 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,19 +1054,20 @@ 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`!",
+          "Found a `DEAD` variable " + name2string(symbol.get_identifier()) +
+            " without corresponding `DECL`!",
           instruction_it->source_location());
       }
     }