Merge pull request #4935 from diffblue/ACSL-quantifier

ACSL quantifiers

Author: tautschnig

regression/cbmc/ACSL/operators.c

@@ -21,8 +21,15 @@ void relations()
   __CPROVER_assert((− a) == (-a), "−");
 }
 
+void quantifiers()
+{
+  __CPROVER_assert((∀ int i; 1) == 1, "∀");
+  __CPROVER_assert((∃ int i; 1) == 1, "∃");
+}
+
 int main()
 {
   boolean();
   relations();
+  quantifiers();
 }

regression/cbmc/ACSL/quantifier-precedence.c

@@ -0,0 +1,6 @@
+int main()
+{
+  // ∀ binds very weakly.
+  // In particular, 'i' below is in the scope of the quantifier.
+  __CPROVER_assert(∀ int i; 1 ? 1 : i, "∀ binds weakly");
+}

regression/cbmc/ACSL/quantifier-precedence.desc

@@ -0,0 +1,8 @@
+CORE
+quantifier-precedence.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/parser.y

@@ -472,16 +472,6 @@ quantifier_expression:
           mto($$, $5);
           PARSER.pop_scope();
         }
-        | TOK_ACSL_FORALL compound_scope declaration primary_expression
-        {
-          // The precedence of this operator is too high; it is meant
-          // to bind only very weakly.
-          $$=$1;
-          set($$, ID_forall);
-          mto($$, $3);
-          mto($$, $4);
-          PARSER.pop_scope();
-        }
         | TOK_EXISTS compound_scope '{' declaration comma_expression '}'
         {
           $$=$1;
@@ -490,36 +480,26 @@ quantifier_expression:
           mto($$, $5);
           PARSER.pop_scope();
         }
-        | TOK_ACSL_EXISTS compound_scope declaration primary_expression
-        {
-          // The precedence of this operator is too high; it is meant
-          // to bind only very weakly.
-          $$=$1;
-          set($$, ID_exists);
-          mto($$, $3);
-          mto($$, $4);
-          PARSER.pop_scope();
-        }
         ;
 
 loop_invariant_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_LOOP_INVARIANT '(' conditional_expression ')'
+        | TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
         { $$=$3; }
         ;
 
 requires_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_REQUIRES '(' conditional_expression ')'
+        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
         { $$=$3; }
         ;
 
 ensures_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_ENSURES '(' conditional_expression ')'
+        | TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
         { $$=$3; }
         ;
 
@@ -819,6 +799,27 @@ logical_equivalence_expression:
         { binary($$, $1, $2, ID_equal, $3); }
         ;
 
+/* Non-standard, defined by ACSL. Lowest precedence of all operators. */
+ACSL_binding_expression:
+          conditional_expression
+        | TOK_ACSL_FORALL compound_scope declaration ACSL_binding_expression
+        {
+          $$=$1;
+          set($$, ID_forall);
+          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
+        }
+        | TOK_ACSL_EXISTS compound_scope declaration ACSL_binding_expression
+        {
+          $$=$1;
+          set($$, ID_exists);
+          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
+        }
+        ;
+
 conditional_expression:
           logical_equivalence_expression
         | logical_equivalence_expression '?' comma_expression ':' conditional_expression
@@ -838,7 +839,7 @@ conditional_expression:
         ;
 
 assignment_expression:
-          conditional_expression
+          ACSL_binding_expression /* usually conditional_expression */
         | cast_expression '=' assignment_expression
         { binary($$, $1, $2, ID_side_effect, $3); parser_stack($$).set(ID_statement, ID_assign); }
         | cast_expression TOK_MULTASSIGN assignment_expression