Function contracts: modified parser to allow conditional assigns clause targets.

The new syntax for conditional targets is  `c ? t` or `c ? {t1, .., tn}`.

Author: Remi Delmas

src/ansi-c/parser.y

@@ -3297,8 +3297,55 @@ cprover_function_contract:
         | cprover_contract_assigns
         ;
 
+logical_equivalence_expression_list:
+          logical_equivalence_expression
+        {
+          init($$, ID_expression_list);
+          mto($$, $1);
+        }
+        | logical_equivalence_expression_list ',' logical_equivalence_expression
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
+
+assigns_target_expression:
+          logical_equivalence_expression
+        {
+          $$=$1;
+        }
+        | logical_equivalence_expression '?' '{' logical_equivalence_expression_list '}'
+        { 
+          $$=$2;
+          parser_stack($$).id(ID_conditional_assigns_target);
+          mto($$, $1);
+          mto($$, $4);
+        }
+        | logical_equivalence_expression '?' logical_equivalence_expression
+        { $$=$2;
+          parser_stack($$).id(ID_conditional_assigns_target);
+          mto($$, $1);
+          mto($$, $3);
+        }
+        ;
+
+assigns_target_expression_list:
+          assigns_target_expression
+        {
+          init($$, ID_target_list);
+          mto($$, $1);
+        }
+        | assigns_target_expression_list ',' assigns_target_expression
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
 cprover_contract_assigns:
-         TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
+         TOK_CPROVER_ASSIGNS '(' assigns_target_expression_list ')'
         {
           $$=$1;
           set($$, ID_C_spec_assigns);

src/util/irep_ids.def

@@ -578,6 +578,7 @@ IREP_ID_TWO(C_spec_requires, #spec_requires)
 IREP_ID_TWO(C_spec_ensures, #spec_ensures)
 IREP_ID_TWO(C_spec_assigns, #spec_assigns)
 IREP_ID_ONE(target_list)
+IREP_ID_ONE(conditional_assigns_target)
 IREP_ID_ONE(virtual_function)
 IREP_ID_TWO(element_type, element_type)
 IREP_ID_ONE(working_directory)