Added assigns clauses for loops

1. Renamed cprover_contract_assigns_opt to cprover_contract_assigns as it did not have unit production.
2. Created cprover_contract_assigns_opt that supports unit productions
3. Added cprover_contract_assigns_opt to iteration_statement.
4. Renamed loop_invariant_opt to cprover_contract_invariant_opt for consistency.
5. Renamed loop_decreases_opt to cprover_contract_decreases_opt for consistency.

This adds support for parsing assigns clauses for loops.

Author: Aalok Thakkar

src/ansi-c/parser.y

@@ -491,14 +491,14 @@ quantifier_expression:
         }
         ;
 
-loop_invariant_opt:
+cprover_contract_invariant_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
         | TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
         { $$=$3; }
         ;
 
-cprover_decreases_opt:
+cprover_contract_decreases_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
         | TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
@@ -2426,31 +2426,36 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
-          loop_invariant_opt cprover_decreases_opt 
+
+          cprover_contract_assigns_opt
+          cprover_contract_invariant_opt
+          cprover_contract_decreases_opt 
           statement
         {
           $$=$1;
           statement($$, ID_while);
-          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7)));
-
-          if(parser_stack($5).is_not_nil())
-            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($5));
+          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
 
           if(parser_stack($6).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6));
+            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($6));
+
+          if(parser_stack($7).is_not_nil())
+            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7));
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
-          loop_invariant_opt cprover_decreases_opt ';'
+          cprover_contract_assigns_opt
+          cprover_contract_invariant_opt 
+          cprover_contract_decreases_opt ';'
         {
           $$=$1;
           statement($$, ID_dowhile);
           parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
 
-          if(parser_stack($7).is_not_nil())
-            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($7));
-
           if(parser_stack($8).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
+            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($8));
+
+          if(parser_stack($9).is_not_nil())
+            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9));
         }
         | TOK_FOR
           {
@@ -2464,7 +2469,9 @@ iteration_statement:
           '(' declaration_or_expression_statement
               comma_expression_opt ';'
               comma_expression_opt ')'
-              loop_invariant_opt cprover_decreases_opt
+              cprover_contract_assigns_opt
+              cprover_contract_invariant_opt
+              cprover_contract_decreases_opt
           statement
         {
           $$=$1;
@@ -2473,13 +2480,13 @@ iteration_statement:
           mto($$, $4);
           mto($$, $5);
           mto($$, $7);
-          mto($$, $11);
-
-          if(parser_stack($9).is_not_nil())
-            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($9));
+          mto($$, $12);
 
           if(parser_stack($10).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10));
+            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($10));
+
+          if(parser_stack($11).is_not_nil())
+            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($11));
 
           if(PARSER.for_has_scope)
             PARSER.pop_scope(); // remove the C99 for-scope
@@ -3261,10 +3268,10 @@ cprover_function_contract:
           set($$, ID_C_spec_requires);
           mto($$, $3);
         }
-        | cprover_contract_assigns_opt
+        | cprover_contract_assigns
         ;
 
-cprover_contract_assigns_opt:
+cprover_contract_assigns:
          TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
         {
           $$=$1;
@@ -3274,6 +3281,16 @@ cprover_contract_assigns_opt:
         }
         ;
 
+cprover_contract_assigns_opt:
+        /* nothing */
+        { init($$); parser_stack($$).make_nil(); }
+        | cprover_contract_assigns
+        ;
+
+<<<<<<< HEAD
+=======
+
+>>>>>>> 36ca4e761... update
 cprover_function_contract_sequence:
           cprover_function_contract
         | cprover_function_contract_sequence cprover_function_contract
@@ -3289,6 +3306,12 @@ cprover_function_contract_sequence_opt:
         | cprover_function_contract_sequence
         ;
 
+cprover_loop_contract:
+          cprover_contract_assigns_opt
+          loop_invariant_opt
+        | loop_invariant_opt
+        ;
+
 postfixing_abstract_declarator:
           parameter_postfixing_abstract_declarator
         /* The following two rules implement K&R headers! */