More-complete-exhale not applied to exhaling wildcards
mschwerhoff opened this issue · 1 comments
mschwerhoff commented
Since Silicon (unlike Carbon) doesn't reorder conjuncts around wildcards and by default greedily operates on individual heap chunks, the following example verifies:
inhale acc(x.f, 1/2) && acc(y.f, 1/2)
exhale acc(x.f, wildcard) && acc(y.f, 1/2)
The wildcard will be exhaled relative to the chunk for x.f
, which provides sufficient permission, and the chunk for y.f
remains unaffected.
However, when using --enableMoreCompleteExhale
, the program is expected to fail, since x
could alias y
, in which case the wildcard could consume more than 1/2
permissions.
mschwerhoff commented
Resolved with commit 24bfa90