New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Facts involving constants don't propagate to bounds checks #5
Comments
If you want to reproduce this:
The HEAD commit in that branch is what replaces the number with the constant name. |
Thanks for the fix! |
@nigeltao playing with this new feature, I hit a fun "cannot prove" error:
The code in question looks like:
Shouldn't this work? Or what am I missing? |
Ignore my comment above - I wasn't actually running the compiler on that assertion. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Apologies if this bug report is lacking any information or if I missed anything obvious. But I've been playing with this for over twenty minutes, and I cannot figure it out.
I have a piece of code:
And this gets an error:
It seems to me like from those facts, I should be able to prove that
i <= 131072
, since131072 == maxBlockSize
andi <= maxBlockSize
. However, I don't seem to be able to. I have tried multiple asserts, includingassert maxBlockSize == 131072
andassert i <= 131072 via "a <= b: a <= c; c == b"(c:maxBlockSize)
.Here's why I think this is a bug in Wuffs - if I replace all uses of
maxBlockSize
with131072
, the bounds error disappears.The text was updated successfully, but these errors were encountered: