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/ansi_c_convert_type.cpp

@@ -252,9 +252,8 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
-    assigns = to_unary_expr(as_expr).op();
 
-    for(const exprt &operand : assigns.operands())
+    for(const exprt &operand : to_unary_expr(as_expr).op().operands())
     {
       if(
         operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
@@ -265,6 +264,14 @@ void ansi_c_convert_typet::read_rec(const typet &type)
         throw 0;
       }
     }
+
+    if(assigns.is_nil())
+      assigns = to_unary_expr(as_expr).op();
+    else
+    {
+      for(auto &assignment : to_unary_expr(as_expr).op().operands())
+        assigns.add_to_operands(std::move(assignment));
+    }
   }
   else if(type.id() == ID_C_spec_ensures)
   {