-
Notifications
You must be signed in to change notification settings - Fork 40
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
unfolding
body does not admit resources
#606
Comments
Hi Pieter, interesting observation! The tutorial even hints at the opposite:
My guess is that we accidentally forbid in-assertions when adding a consistency checker that prevents impure unfoldings in expression position, in particular function bodies. We'll discuss, and I'll get back to you. |
For what it's worth, Silicon crashes if it gets an impure assertion in this position. So if we get rid of the consistency check, we'll also need to extend the backend(s). |
Viper disallows putting resource assertions in the body of an
unfolding
:reports in the Viper IDE:
I noticed that this is not mentioned in the tutorial, so I was wondering whether there is a technical reason that this is not allowed?
Also, I suspect it may be possible to desugar impure unfolding expressions into pure ones, by pushing in the unfolding into the pure bits of the expression (
unfolding pr() in acc(x.f, p)
->acc((unfolding pr() in x).f, unfolding pr() in p)
,unfolding pr() in x && y
->(unfolding pr() in x) && (unfolding pr() in y)
, etc.). We're considering implementing that, so I'm also interested in whether you would implement something like this, or see a glaring flaw with this plan.The text was updated successfully, but these errors were encountered: