Created cprover_loop_contract

1. Created cprover_loop_contract that has loop_invariant_opt and cprover_contract_assigns_opt.
2. Created cprover_loop_contract_sequence_opt.
3. Added cprover_loop_contract_sequence_opt to iteration_statement for all three types of loops.

This adds support for parsing assigns clauses for loops.

Author: Aalok Thakkar

src/ansi-c/parser.y

@@ -2418,7 +2418,7 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
-          loop_invariant_opt statement
+          cprover_loop_contract_sequence_opt statement
         {
           $$=$1;
           statement($$, ID_while);
@@ -2428,7 +2428,7 @@ iteration_statement:
             parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($5));
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
-          loop_invariant_opt ';'
+          cprover_loop_contract_sequence_opt ';'
         {
           $$=$1;
           statement($$, ID_dowhile);
@@ -2449,7 +2449,7 @@ iteration_statement:
           '(' declaration_or_expression_statement
               comma_expression_opt ';'
               comma_expression_opt ')'
-              loop_invariant_opt
+              cprover_loop_contract_sequence_opt
           statement
         {
           $$=$1;
@@ -3269,6 +3269,23 @@ cprover_function_contract_sequence_opt:
           /* nothing */
           { init($$); }
         | cprover_function_contract_sequence
+<<<<<<< HEAD
+=======
+        ;
+
+cprover_loop_contract:
+          loop_invariant_opt
+        | cprover_contract_assigns_opt
+        ;
+
+cprover_loop_contract_sequence_opt:
+          cprover_loop_contract
+        | cprover_loop_contract_sequence_opt cprover_loop_contract
+        {
+          $$=$1;
+          merge($$, $2);
+        }
+>>>>>>> 863623ddd... Created cprover_loop_contract
         ;
 
 postfixing_abstract_declarator: