Skip to content
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

Add Inhaling expression #799

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from

Conversation

manud99
Copy link
Contributor

@manud99 manud99 commented Jun 11, 2024

@JonasAlaif and I have been working on a new inhaling expression. The purpose of this new expression is that we want to temporarily inhale some assertion to check facts that are inaccessible in the current state. An example of this is a magic wand, where we don't hold its LHS and where we want to check a property in the snapshot of this magic wand.

For example, we can use this expression to define the snapshot of a wand as follows:

field f: Int

method test5(x: Ref, y: Ref)
    requires true --* acc(x.f)
    requires acc(x.f) --* acc(y.f)
    requires inhaling (acc(x.f)) in applying (acc(x.f) --* acc(y.f)) in y.f == 10
{
    apply true --* acc(x.f)
    apply acc(x.f) --* acc(y.f)

    assert y.f == 10
}

The syntax is as follows: inhaling (<assertion>) in <expression>

This PR extends Silver to parse this new expression and adds some test files to check the expected behavior. There is also an implementation for Silicon in viperproject/silicon#848.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant