reject contracts on do/while loops for now

Whether the first (unguarded) loop iteration should be executed "before"
the base case assertion or not is still under discussion.
Loop contracts on do/while loops are rejected until this is resolved.

Author: SaswatPadhi

regression/contracts/loop_contracts_do_while/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+
+  do
+  {
+    x++;
+  } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10);
+
+  assert(x == 10);
+}

regression/contracts/loop_contracts_do_while/test.desc

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

src/goto-instrument/contracts/contracts.cpp

@@ -236,10 +236,14 @@ void code_contractst::check_apply_loop_contracts(
     new_decreases_vars.push_back(new_decreases_var);
   }
 
-  // non-deterministically skip the loop if it is a do-while loop.
   // TODO: Fix loop contract issues for do/while loops.
   if(!loop_head->is_goto())
   {
+    log.error() << "Loop contracts are unsupported on do/while loops: "
+                << loop_head->source_location() << messaget::eom;
+    throw 0;
+
+    // non-deterministically skip the loop if it is a do-while loop.
     generated_code.add(goto_programt::make_goto(
       loop_end,
       side_effect_expr_nondett(bool_typet(), loop_head->source_location())));