make trigger-generation code less sensitive to arithmetic

[viper-admin]

Created by @alexanderjsummers on 2014-11-10 14:32
Last updated on 2018-06-09 12:24

In some cases, trigger generation is sensitive to the way in which arithmetic is expressed, since arithmetic operations are ruled out in triggers. We could try to automatically rewrite such quantifiers, instead of failing to find triggers for them. For example:

//invariant forall j:Int :: 0<=j && j < n && (x+j) in [0..length(a)) && (y+j) in [0..length(a)) ==> loc(a,x+j).val == loc(a,y+j).val // no triggers involving loc are available
// REWRITTEN USING: j==k-x, k==j+x
invariant forall k:Int :: x<=k && k < x+n ==> loc(a,k).val == loc(a,y+k-x).val // triggers on loc(a,k)

[viper-admin]

@mschwerhoff commented on 2018-06-09 12:24

Also see all/issues/silver/0067.sil, which was originally reported as Silicon issue #251 and Carbon issue #159.