Revisit triggers chosen for quantified inhale /exhale (especially of predicates)

[viper-admin]

Created by @alexanderjsummers on 2018-06-05 16:14 Last updated on 2018-06-06 09:42

The existing code selects triggers slightly differently on inhale and on exhale. In addition (as commented in the code) it would be better to use the underlying Boogie representation of a predicate instance (the function mapping to a field on the heap) as a default trigger (unlike for fields, this either works, or none of the lookups on this predicate will work); for fields, the receiver expression is tried but may not work if it is simply the quantified variable x.

This code should be revisited (and ideally also cleaned up to remove duplication).

[viper-admin]

@alexanderjsummers commented on 2018-06-06 09:42

At the moment, Carbon also selects the location for the QP as a trigger, both in the Heap and in the Mask (for permission lookup). This is in part because we don't have a clear design for handling heap-dependent triggers in general; it seems it would be better for the default behaviour to be that a trigger x.f gets translated as both of these kinds of lookups (or as some term which both of these lookups would generate).