Using Magic Wands in Fractional Predicates Results in Unsoundnesses

[viper-admin]

Created by bitbucket user nilsbecker_ on 2017-09-06 20:26

The current implementation always consumes and produces magic wand chunks with write permissions. When unfolding half a predicate that contains a magic wand, the full wand is, therefore, produced. This can lead to unsoundnesses since magic wands and the permissions contained in their footprints can be duplicated, as shown in the attached Viper program.

---

Attachments:

• wandInFractionalPredicate.sil