Skip to content

Incorrect encoding when predicate arguments in fold contain permission introspection #577

@Dev-XYS

Description

@Dev-XYS

Related to #568.

The same bug occurs in fold statements as well.

field f: Int

predicate P(x: Ref, p: Perm)
{
    acc(x.f)
}

method foo(x: Ref)
    requires acc(x.f)
{
    fold P(x, perm(x.f))
    assert P(x, write)    // Verification fails.
}

Different to #568, the bug also affects permission introspection to heap locations in the predicate body, since Carbon first exhales predicate body before inhaling the predicate instance.

Metadata

Metadata

Assignees

Labels

bugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions