Maintain loop invariant annotation when converting do .. while

With the changes in bbd9de4 we newly made do .. while converted
instructions subject to `optimize_guarded_gotos`, which previously
rewrote conditions without retaining annotations related to loop
invariants.

The included tests now show that the annotations are preserved, but
still fail for an unrelated bug in how do .. while loops are
instrumented.

Author: tautschnig

regression/contracts-dfcc/loop_contracts_do_while/assigns.c

@@ -0,0 +1,19 @@
+int global;
+
+int main()
+{
+  global = 0;
+  int argc = 1;
+  if(argc > 1)
+  {
+    do
+      __CPROVER_assigns(global)
+      {
+        global = 1;
+      }
+    while(0);
+  }
+  __CPROVER_assert(global == 0, "should be zero");
+
+  return 0;
+}

regression/contracts-dfcc/loop_contracts_do_while/assigns.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+assigns.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that loop contracts work correctly on do/while loops.

regression/contracts-dfcc/loop_contracts_do_while/main.c

@@ -5,7 +5,7 @@ int main()
   int x = 0;
 
   do
-    __CPROVER_loop_invariant(0 <= x && x <= 10)
+    __CPROVER_loop_invariant(0 <= x && x < 10)
     {
       x++;
     }

regression/contracts-dfcc/loop_contracts_do_while/side_effect.c

@@ -0,0 +1,24 @@
+int global;
+
+int foo()
+{
+  return 0;
+}
+
+int main()
+{
+  global = 0;
+  int argc = 1;
+  if(argc > 1)
+  {
+    do
+      __CPROVER_assigns(global)
+      {
+        global = 1;
+      }
+    while(foo());
+  }
+  __CPROVER_assert(global == 0, "should be zero");
+
+  return 0;
+}

regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+side_effect.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that loop contracts work correctly on do/while loops.

regression/contracts-dfcc/loop_contracts_do_while/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$

regression/contracts/loop_contracts_do_while/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --apply-loop-contracts
 ^EXIT=0$
@@ -7,3 +7,4 @@ main.c
 --
 --
 This test checks that loop contracts work correctly on do/while loops.
+Fails because contracts are not yet supported on do while loops.

src/ansi-c/goto-conversion/goto_convert.cpp

@@ -432,8 +432,25 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
     // cannot compare iterators, so compare target number instead
     if(it->get_target()->target_number == it_z->target_number)
     {
+      DATA_INVARIANT(
+        it->condition().find(ID_C_spec_assigns).is_nil() &&
+          it->condition().find(ID_C_spec_loop_invariant).is_nil() &&
+          it->condition().find(ID_C_spec_decreases).is_nil(),
+        "no loop invariant expected");
+      irept y_assigns = it_goto_y->condition().find(ID_C_spec_assigns);
+      irept y_loop_invariant =
+        it_goto_y->condition().find(ID_C_spec_loop_invariant);
+      irept y_decreases = it_goto_y->condition().find(ID_C_spec_decreases);
+
       it->set_target(it_goto_y->get_target());
-      it->condition_nonconst() = boolean_negate(it->condition());
+      exprt updated_condition = boolean_negate(it->condition());
+      if(y_assigns.is_not_nil())
+        updated_condition.add(ID_C_spec_assigns).swap(y_assigns);
+      if(y_loop_invariant.is_not_nil())
+        updated_condition.add(ID_C_spec_loop_invariant).swap(y_loop_invariant);
+      if(y_decreases.is_not_nil())
+        updated_condition.add(ID_C_spec_decreases).swap(y_decreases);
+      it->condition_nonconst() = updated_condition;
       it_goto_y->turn_into_skip();
     }
   }
@@ -1301,7 +1318,7 @@ void goto_convertt::convert_dowhile(
   W->complete_goto(w);
 
   // assigns_clause, loop invariant and decreases clause
-  convert_loop_contracts(code, y);
+  convert_loop_contracts(code, W);
 
   dest.destructive_append(tmp_w);
   dest.destructive_append(side_effects.side_effects);