Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
@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:
The syntax is as follows:
inhaling (<assertion>) in <expression>
assertion
must be in parenthesis because of a conflict with thein
keyword used for sets. This has been discussed for the applying expression in Backtracking Not Working After "in" Keyword #216.expression
must be pure.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.