viper-admin
viper-admin
> Created by **@alexanderjsummers** on 2019-10-30 08:47 Because of how loops are verified, the current meaning of an “invariant” on a label varies significantly depending on whether the label represents...
> Created by **@mschwerhoff** on 2017-03-31 13:32 Currently fails, most likely due to an incompleteness in Z3: ```text inhale 0
> Created by **@alexanderjsummers** on 2020-01-13 16:57 For both Silicon and Carbon there are parallelization options to disable, different ways to pass a random seed to Z3, and ways to...
> Created by bitbucket user **OmerSakar** on 2019-12-13 16:23 See issues on the Silicon and Carbon projects: [https://github.com/viperproject/silicon/issues/405](https://github.com/viperproject/silicon/issues/405) [https://github.com/viperproject/carbon/issues/292](https://github.com/viperproject/carbon/issues/292)
> Created by **@mschwerhoff** on 2019-09-03 16:05 Parser errors, such as reported for the snippet ```plaintext field nxt: Ref predicate P(x) { true } ``` are currently not properly recognised...
> Created by **@mschwerhoff** on 2015-12-03 15:40 > Last updated on 2019-08-28 10:56
> Created by **@alexanderjsummers** on 2019-08-28 10:02 The file uses `now` as a construct; this doesn’t exist in recent Viper. Instead, one should use e.g. labelled-old expressions referring to a...
> Created by bitbucket user **nilsbecker_** on 2017-09-06 22:14 > Last updated on 2019-07-31 09:29 `in` can either be parsed as a set operation or as part of a `let`,...
> Created by **@mschwerhoff** on 2019-07-28 12:29 > Last updated on 2019-07-28 12:30 The Silver test suite currently has the following directory structures: ```plaintext all assume basic chalice domains functions...
> Created by **@mschwerhoff** on 2019-03-23 22:14 > Last updated on 2019-07-28 12:30 The Viper test suite is currently executed as follows: the test runner (instances of `viper.silver.testing.SilSuite`, see e.g....