Clarify "effective" semantics of magic wands in Viper

[viper-admin]

Created by @mschwerhoff on 2015-12-03 15:40
Last updated on 2019-08-28 10:56

[viper-admin]

@mschwerhoff commented on 2015-12-03 15:43

See wands\regression\potential_unsoundness.sil

[viper-admin]

@mschwerhoff commented on 2017-12-06 15:13

The degree to which wands are treated syntactically (upon lookup), i.e. which subexpressions are treated as holes/are compared semantically, should also be clarified. It should also be documented, e.g. in the tutorial. See also #230.

[viper-admin]

@alexanderjsummers commented on 2019-08-28 10:56

See the tutorial issue: https://bitbucket.org/viperproject/tutorial/issues/3/clarify-how-magic-wand-instances-are

[viper-admin]

@alexanderjsummers commented on 2019-08-28 10:56

We should make sure the interesting cases are handled in the test suite, for the sake of closing this particular (Silver) issue