allow multiple assigns clauses

This changes the parser to allow multiple assigns clauses in a contract.
The meaning of multiple clauses is the same as the meaning of one clause
that contains the concatenation of the target lists of the given clauses.

Author: kroening

regression/contracts/assigns_enforce_03/main.c

@@ -8,7 +8,8 @@ void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
   f3(x2, y2, z2);
 }
 
-void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3) __CPROVER_assigns(*y3)
+  __CPROVER_assigns(*z3)
 {
   *x3 = *x3 + 1;
   *y3 = *y3 + 1;

src/ansi-c/parser.y

@@ -2437,7 +2437,7 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
-          cprover_contract_assigns_opt
+          cprover_contract_assigns_list_opt
           cprover_contract_loop_invariant_list_opt 
           cprover_contract_decreases_opt
           statement
@@ -2453,7 +2453,7 @@ iteration_statement:
             parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7));
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
-          cprover_contract_assigns_opt
+          cprover_contract_assigns_list_opt
           cprover_contract_loop_invariant_list_opt 
           cprover_contract_decreases_opt ';'
         {
@@ -2479,7 +2479,7 @@ iteration_statement:
           '(' declaration_or_expression_statement
               comma_expression_opt ';'
               comma_expression_opt ')'
-              cprover_contract_assigns_opt
+              cprover_contract_assigns_list_opt
               cprover_contract_loop_invariant_list_opt 
               cprover_contract_decreases_opt
           statement
@@ -3297,10 +3297,20 @@ cprover_contract_assigns:
         }
         ;
 
-cprover_contract_assigns_opt:
+cprover_contract_assigns_list:
+          cprover_contract_assigns
+        | cprover_contract_assigns_list cprover_contract_assigns
+        {
+          $$=$1;
+          for(auto &target : parser_stack($2).operands())
+            parser_stack($$).add_to_operands(std::move(target));
+        }
+        ;
+
+cprover_contract_assigns_list_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | cprover_contract_assigns
+        | cprover_contract_assigns_list
         ;
 
 cprover_function_contract_sequence: