silver
silver copied to clipboard
viperproject
Trigger generation may generate triggers which don't work at call site
Created by @alexanderjsummers on 2016-10-18 17:53 Last updated on 2016-10-18 18:04
Trigger generation for quantifiers occurring in e.g. method contracts will decide which terms are valid in triggers based on the signatures with formal parameters. However, at call-site the back-ends will typically substitute actuals for formals. This substitution must happen in quantifier triggers too (otherwise we would generate nonsense terms which didn't match), but this might create terms which are not allowed in triggers.
@alexanderjsummers commented on 2016-10-18 18:04
also affects resources\quantifiedpermissions\third_party\testHistogram.sil (at least, once choosing triggers for quantified permissions) - disabled for now
@alexanderjsummers commented on 2016-10-19 10:59
https://github.com/viperproject/silver/issues/97 was marked as a duplicate of this issue.