viper-admin

> Created by **@alexanderjsummers** on 2017-08-08 19:30 This seems likely to be related to fold/unfold issues with performance. The example verifies rather fast with Silicon. --- Attachments: * [**`morris_ext.vpr`**](https://gist.githubusercontent.com/viper-admin/f3d0f8941b9b2c6431234d397d621775/raw/4a5bce97e32559fa2b93e3ef8110128b41a22ab6/morris_ext.vpr)

> Created by **@vakaras** on 2018-07-23 16:09 This program: ``` #!silver field val: Int domain Array { function loc(arr: Array, pos: Int): Ref function len(arr: Array): Int } predicate arrayacc(a:...

Mentioning recursive function body in its postcondition leads to a matching loop

1

> Created by **@vakaras** on 2018-07-25 09:14 > Last updated on 2018-07-25 09:15 The functions `fib3` and `fib4` below cause matching loops as illustrated with asserts in the methods `test3`...

A heap-dependent function can lead to a matching loop without any explicit quantifiers

1

> Created by **@vakaras** on 2018-07-25 09:07 > Last updated on 2018-07-25 09:16 The function `fib2` below causes a matching loop as illustrated with an assert in the method `test2`...

> Created by **@alexanderjsummers** on 2018-09-20 09:52 Examples in which many heaps and masks are generated via the Boogie encoding become slow; this seems at least partly because every lookup...

> Created by **@alexanderjsummers** on 2018-09-26 07:26 Comments there suggest that we will potentially generate quantifiers without explicitly selected triggers (in cases in which type variables are introduced). We should...

Permission constraint not deduced for example all/assume/assume10QP.sil

7

> Created by **@mschwerhoff** on 2018-10-12 13:59 > Last updated on 2018-10-12 16:28 The gist of the example is the following: ```text inhale acc(x.f, p) assume (forall y: Ref ::...

Investigate comment on line 94 of DefaultStateModule.scala

1

> Created by **@alexanderjsummers** on 2019-02-19 18:15 It seems there could be a subtle issue with respect to when old heaps/masks are used; this needs double-checking.

> Created by **@alexanderjsummers** on 2019-03-10 18:07 The pattern-match uses underscores to mask certain sub-expressions; although unlikely, it should be possible to write terms in these positions which are not...

Several test suite files consume too much memory

1

> Created by **@alexanderjsummers** on 2019-08-16 15:40 > Last updated on 2019-11-18 13:22 This is likely due to matching loops in the files, but should be investigated. The files are:...