Applying expressions potentially unsound

[viper-admin]

Created by @mschwerhoff on 2017-09-25 09:03

The current implementation of magic wand snapshots can result in contradicting assumptions (i.e. is unsound) if a magic wand (chunk) is applied more than once. This can be achieved using applying expressions, as illustrated in attached file test205.sil. A discussion of the problem, as well as a solution, can be found in my thesis and in Nils Becker's project report.

---

Attachments:

• test205.sil