Allow loop contracts annotated to GOTO statement

Author: qinheping

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

@@ -1005,12 +1005,12 @@ void goto_convertt::convert_assume(
 void goto_convertt::convert_loop_contracts(
   const codet &code,
   goto_programt::targett loop,
-  const irep_idt &mode)
+  bool check_side_effect)
 {
   auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
   if(assigns.is_not_nil())
   {
-    PRECONDITION(loop->is_goto());
+    PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
     loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
   }
 
@@ -1020,11 +1020,20 @@ void goto_convertt::convert_loop_contracts(
   {
     if(has_subexpr(invariant, ID_side_effect))
     {
-      throw incorrect_goto_program_exceptiont(
-        "Loop invariant is not side-effect free.", code.find_source_location());
+      if(check_side_effect)
+      {
+        throw incorrect_goto_program_exceptiont(
+          "Loop invariant is not side-effect free.",
+          code.find_source_location());
+      }
+      else
+      {
+        warning().source_location = code.find_source_location();
+        warning() << "Loop invariants is not side-effect-free." << eom;
+      }
     }
 
-    PRECONDITION(loop->is_goto());
+    PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
     loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
   }
 
@@ -1034,12 +1043,20 @@ void goto_convertt::convert_loop_contracts(
   {
     if(has_subexpr(decreases_clause, ID_side_effect))
     {
-      throw incorrect_goto_program_exceptiont(
-        "Decreases clause is not side-effect free.",
-        code.find_source_location());
+      if(check_side_effect)
+      {
+        throw incorrect_goto_program_exceptiont(
+          "Decreases clause is not side-effect free.",
+          code.find_source_location());
+      }
+      else
+      {
+        warning().source_location = code.find_source_location();
+        warning() << "Decreases clause is not side-effect-free." << eom;
+      }
     }
 
-    PRECONDITION(loop->is_goto());
+    PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
     loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
   }
 }
@@ -1123,7 +1140,7 @@ void goto_convertt::convert_for(
     goto_programt::make_goto(u, true_exprt(), code.source_location()));
 
   // assigns clause, loop invariant and decreases clause
-  convert_loop_contracts(code, y, mode);
+  convert_loop_contracts(code, y);
 
   dest.destructive_append(sideeffects);
   dest.destructive_append(tmp_v);
@@ -1181,7 +1198,7 @@ void goto_convertt::convert_while(
   convert(code.body(), tmp_x, mode);
 
   // assigns clause, loop invariant and decreases clause
-  convert_loop_contracts(code, y, mode);
+  convert_loop_contracts(code, y);
 
   dest.destructive_append(tmp_branch);
   dest.destructive_append(tmp_x);
@@ -1250,7 +1267,7 @@ void goto_convertt::convert_dowhile(
   y->complete_goto(w);
 
   // assigns_clause, loop invariant and decreases clause
-  convert_loop_contracts(code, y, mode);
+  convert_loop_contracts(code, y);
 
   dest.destructive_append(tmp_w);
   dest.destructive_append(sideeffects);
@@ -1512,6 +1529,9 @@ void goto_convertt::convert_goto(const code_gotot &code, goto_programt &dest)
   goto_programt::targett t =
     dest.add(goto_programt::make_incomplete_goto(code, code.source_location()));
 
+  // Loop contracts annotated in GOTO
+  convert_loop_contracts(code, t, false);
+
   // remember it to do the target later
   targets.gotos.emplace_back(t, targets.scope_stack.get_current_node());
 }

src/ansi-c/goto-conversion/goto_convert_class.h

@@ -244,7 +244,7 @@ class goto_convertt : public messaget
   void convert_loop_contracts(
     const codet &code,
     goto_programt::targett loop,
-    const irep_idt &mode);
+    bool check_side_effect = true);
   void
   convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
   void convert_while(