Support desugaring of nested quantified permissions

[viper-admin]

Created by @alexanderjsummers on 2018-10-03 16:09 Last updated on 2018-10-03 16:12

The current rules in the AST (see the QuantifiedPermissions object) rewrite certain special cases of quantified permissions into a standard form (that the backends then use), but do not cover all cases. In particular, various kinds of nesting get missed, and then cause failures in the back-ends. One example is below:

#!scala
field integer__item: Int

method minimal_example(xs: Seq[Ref], m: Int, n: Int)
requires m*n == |xs|
requires (forall i: Int :: 0<=i && i<m ==> (forall j: Int :: (i*n)<=j && j<((i+1)*n) ==> acc(xs[j].integer__item, 1/2)))
{

}

another can be found in https://github.com/viperproject/silver/issues/175

[viper-admin]

@alexanderjsummers commented on 2018-10-03 16:12

Thanks to HMulder for reporting the example