Maintain loop invariant annotation when converting do .. while

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 @@
+CORE dfcc-only
+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 @@
+CORE dfcc-only
+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 @@
     // 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 @@
   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);

src/goto-instrument/contracts/utils.cpp

@@ -250,7 +250,7 @@ void insert_before_and_update_jumps(
   const auto new_target = destination.insert_before(target, i);
   for(auto it : target->incoming_edges)
   {
-    if(it->is_goto())
+    if(it->is_goto() && it->get_target() == target)
       it->set_target(new_target);
   }
 }