Skip to content

Commit e9fdbe9

Browse files
author
Daniel Kroening
committed
fix precedence of ACSL forall/exist
The precedence now matches what the standard requires.
1 parent 3ef0f30 commit e9fdbe9

File tree

2 files changed

+26
-25
lines changed

2 files changed

+26
-25
lines changed

regression/cbmc/ACSL/quantifier-precedence.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
quantifier-precedence.c
33

44
^EXIT=0$

src/ansi-c/parser.y

Lines changed: 25 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -472,16 +472,6 @@ quantifier_expression:
472472
mto($$, $5);
473473
PARSER.pop_scope();
474474
}
475-
| TOK_ACSL_FORALL compound_scope declaration primary_expression
476-
{
477-
// The precedence of this operator is too high; it is meant
478-
// to bind only very weakly.
479-
$$=$1;
480-
set($$, ID_forall);
481-
mto($$, $3);
482-
mto($$, $4);
483-
PARSER.pop_scope();
484-
}
485475
| TOK_EXISTS compound_scope '{' declaration comma_expression '}'
486476
{
487477
$$=$1;
@@ -490,36 +480,26 @@ quantifier_expression:
490480
mto($$, $5);
491481
PARSER.pop_scope();
492482
}
493-
| TOK_ACSL_EXISTS compound_scope declaration primary_expression
494-
{
495-
// The precedence of this operator is too high; it is meant
496-
// to bind only very weakly.
497-
$$=$1;
498-
set($$, ID_exists);
499-
mto($$, $3);
500-
mto($$, $4);
501-
PARSER.pop_scope();
502-
}
503483
;
504484

505485
loop_invariant_opt:
506486
/* nothing */
507487
{ init($$); parser_stack($$).make_nil(); }
508-
| TOK_CPROVER_LOOP_INVARIANT '(' conditional_expression ')'
488+
| TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
509489
{ $$=$3; }
510490
;
511491

512492
requires_opt:
513493
/* nothing */
514494
{ init($$); parser_stack($$).make_nil(); }
515-
| TOK_CPROVER_REQUIRES '(' conditional_expression ')'
495+
| TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
516496
{ $$=$3; }
517497
;
518498

519499
ensures_opt:
520500
/* nothing */
521501
{ init($$); parser_stack($$).make_nil(); }
522-
| TOK_CPROVER_ENSURES '(' conditional_expression ')'
502+
| TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
523503
{ $$=$3; }
524504
;
525505

@@ -819,6 +799,27 @@ logical_equivalence_expression:
819799
{ binary($$, $1, $2, ID_equal, $3); }
820800
;
821801

802+
/* Non-standard, defined by ACSL. Lowest precedence of all operators. */
803+
ACSL_binding_expression:
804+
conditional_expression
805+
| TOK_ACSL_FORALL compound_scope declaration ACSL_binding_expression
806+
{
807+
$$=$1;
808+
set($$, ID_forall);
809+
mto($$, $3);
810+
mto($$, $4);
811+
PARSER.pop_scope();
812+
}
813+
| TOK_ACSL_EXISTS compound_scope declaration ACSL_binding_expression
814+
{
815+
$$=$1;
816+
set($$, ID_exists);
817+
mto($$, $3);
818+
mto($$, $4);
819+
PARSER.pop_scope();
820+
}
821+
;
822+
822823
conditional_expression:
823824
logical_equivalence_expression
824825
| logical_equivalence_expression '?' comma_expression ':' conditional_expression
@@ -838,7 +839,7 @@ conditional_expression:
838839
;
839840

840841
assignment_expression:
841-
conditional_expression
842+
ACSL_binding_expression /* usually conditional_expression */
842843
| cast_expression '=' assignment_expression
843844
{ binary($$, $1, $2, ID_side_effect, $3); parser_stack($$).set(ID_statement, ID_assign); }
844845
| cast_expression TOK_MULTASSIGN assignment_expression

0 commit comments

Comments
 (0)