allow multiple loop invariants

This extends the grammar to allow multiple loop invariants for one loop.

Author: kroening

regression/contracts/invar_check_multiple_loops/main.c

@@ -7,7 +7,8 @@ int main()
 
   for(r = 0; r < n; ++r)
     // clang-format off
-    __CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
+    __CPROVER_loop_invariant(0 <= r && r <= n)
+    __CPROVER_loop_invariant(x == y + r)
     __CPROVER_decreases(n - r)
     // clang-format on
     {

src/ansi-c/c_typecheck_code.cpp

@@ -815,10 +815,12 @@ void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
 {
   if(code.find(ID_C_spec_loop_invariant).is_not_nil())
   {
-    exprt &invariant = static_cast<exprt &>(code.add(ID_C_spec_loop_invariant));
-
-    typecheck_expr(invariant);
-    implicit_typecast_bool(invariant);
+    for(auto &invariant :
+        (static_cast<exprt &>(code.add(ID_C_spec_loop_invariant)).operands()))
+    {
+      typecheck_expr(invariant);
+      implicit_typecast_bool(invariant);
+    }
   }
 }
 

src/ansi-c/parser.y

@@ -491,11 +491,22 @@ quantifier_expression:
         }
         ;
 
-loop_invariant_opt:
+loop_invariant:
+          TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
+        { $$=$3; }
+        ;
+
+loop_invariant_list:
+          loop_invariant
+        { init($$); mto($$, $1); }
+        | loop_invariant_list loop_invariant
+        { $$=$1; mto($$, $2); }
+        ;
+
+loop_invariant_list_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
-        { $$=$3; }
+        | loop_invariant_list
         ;
 
 cprover_decreases_opt:
@@ -2426,7 +2437,7 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
-          loop_invariant_opt cprover_decreases_opt 
+          loop_invariant_list_opt cprover_decreases_opt
           statement
         {
           $$=$1;
@@ -2440,7 +2451,7 @@ iteration_statement:
             parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6));
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
-          loop_invariant_opt cprover_decreases_opt ';'
+          loop_invariant_list_opt cprover_decreases_opt ';'
         {
           $$=$1;
           statement($$, ID_dowhile);
@@ -2464,7 +2475,7 @@ iteration_statement:
           '(' declaration_or_expression_statement
               comma_expression_opt ';'
               comma_expression_opt ')'
-              loop_invariant_opt cprover_decreases_opt
+              loop_invariant_list_opt cprover_decreases_opt
           statement
         {
           $$=$1;

src/goto-instrument/code_contracts.cpp

@@ -149,6 +149,11 @@ void code_contractst::check_apply_loop_contracts(
         << messaget::eom;
     }
   }
+  else
+  {
+    // form the conjunction
+    invariant = conjunction(invariant.operands());
+  }
 
   // change
   //   H: loop;