Merge pull request #8380 from tautschnig/bugfixes/contract-scope-8337

C front-end: place requires and ensures in designated scope

Author: kroening

regression/ansi-c/contracts_scope1/main.c

@@ -0,0 +1,28 @@
+#define C 8
+
+typedef unsigned st[C];
+
+// clang-format off
+void init_st(st dst)
+  __CPROVER_requires(__CPROVER_is_fresh(dst, sizeof(st)))
+  __CPROVER_assigns(__CPROVER_object_whole(dst))
+  __CPROVER_ensures(__CPROVER_forall {
+    unsigned i; (0 <= i && i < C) ==> dst[i] == 0
+  });
+// clang-format on
+
+void init_st(st dst)
+{
+  __CPROVER_size_t i;
+  for(i = 0; i < C; i++)
+  {
+    dst[i] = 0;
+  }
+}
+
+int main()
+{
+  st dest;
+
+  init_st(dest);
+}

regression/ansi-c/contracts_scope1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/parser.y

@@ -3337,17 +3337,27 @@ parameter_abstract_declarator:
         ;
 
 cprover_function_contract:
-          TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
+          TOK_CPROVER_ENSURES
+        {
+          PARSER.new_scope("ensures::");
+        }
+          '(' ACSL_binding_expression ')'
         {
           $$=$1;
           set($$, ID_C_spec_ensures);
-          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
         }
-        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
+        | TOK_CPROVER_REQUIRES
+        {
+          PARSER.new_scope("requires::");
+        }
+          '(' ACSL_binding_expression ')'
         {
           $$=$1;
           set($$, ID_C_spec_requires);
-          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
         }
         | cprover_contract_assigns
         | cprover_contract_frees