You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As an example, consider the list_copy specification:
{ r :-> x ** lseg(x, S) }
void listcopy(loc r)
{ r :-> y ** lseg(x, S) ** lseg(y, S) }
It would be nice to be able to state something like
{ r :-> x ** [lseg(x, S)] }
in the precondition to indicate that this lseg is not to be unfolded during the synthesis. In the future, the syntax may be enhanced with fractional permissions.
This issue is about AST/parsing only. It does not cover the semantics of read-only permissions.
The text was updated successfully, but these errors were encountered:
As an example, consider the
list_copy
specification:It would be nice to be able to state something like
in the precondition to indicate that this
lseg
is not to be unfolded during the synthesis. In the future, the syntax may be enhanced with fractional permissions.This issue is about AST/parsing only. It does not cover the semantics of read-only permissions.
The text was updated successfully, but these errors were encountered: