reject contracts on do/while loops for now

Author: SaswatPadhi

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 currently 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())));