viperproject/silicon

More-complete-exhale not applied to exhaling wildcards

mschwerhoff opened this issue · 1 comments

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.

Resolved with commit 24bfa90