The following program should verify thanks to known-folded permissions, but does not:
field val: Int
predicate knownFolded(x: Ref) {
acc(x.val, 1/2)
}
method test(x: Ref, y: Ref)
requires acc(x.val, 1/2) && x.val == 5
requires acc(y.val)
{
fold knownFolded(x)
exhale acc(y.val)
inhale acc(x.val, 1/2)
assert x.val == 5
}
The following program should verify thanks to known-folded permissions, but does not: