Merge pull request #6177 from diffblue/empty_assigns_clause

Allow an empty assigns clause

Author: feliperodri

regression/contracts/assigns_enforce_15/main.c

@@ -20,10 +20,16 @@ int baz() __CPROVER_ensures(__CPROVER_return_value == global)
   return global;
 }
 
+void qux(void) __CPROVER_assigns()
+{
+  global = global + 1;
+}
+
 int main()
 {
   int n;
   n = foo(&n);
   n = baz();
+  qux();
   return 0;
 }

regression/contracts/assigns_enforce_15/test.desc

@@ -3,8 +3,9 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[bar.1\] line \d+ .*: FAILURE$
-^\[baz.1\] line \d+ .*: FAILURE$
+^\[bar\.1\] line \d+ .*: FAILURE$
+^\[baz\.1\] line \d+ .*: FAILURE$
+^\[qux\.1\] line \d+ .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

src/ansi-c/parser.y

@@ -3272,6 +3272,12 @@ cprover_contract_assigns_opt:
           parser_stack($3).id(ID_target_list);
           mto($$, $3);
         }
+        | TOK_CPROVER_ASSIGNS '(' ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_assigns);
+          parser_stack($$).add_to_operands(exprt(ID_target_list));
+        }
         ;
 
 cprover_function_contract_sequence: