Fix handling of DEAD instructions and function call inlining

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(