Skip to content

Commit 3ef0f30

Browse files
author
Daniel Kroening
committed
knownbug: precedence of ACSL quantifiers
The ACSL quantifiers bind very weakly -- the current grammar assumes a very strong binding.
1 parent 8b91325 commit 3ef0f30

File tree

2 files changed

+14
-0
lines changed

2 files changed

+14
-0
lines changed
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int main()
2+
{
3+
// ∀ binds very weakly.
4+
// In particular, 'i' below is in the scope of the quantifier.
5+
__CPROVER_assert(∀ int i; 1 ? 1 : i, "∀ binds weakly");
6+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
quantifier-precedence.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

0 commit comments

Comments
 (0)