viper-admin
viper-admin
> Created by bitbucket user **abdelzaher** on 2018-05-22 20:51 > Last updated on 2018-05-23 15:09 Here this example verifies as the package statement seems to lead us into some inconsistent...
> Created by bitbucket user **ykass** on 2014-08-21 08:41 > Last updated on 2018-05-13 13:50 The verification of the attached file fails. Silicon can unfold the function definition in the...
> Created by **@mschwerhoff** on 2018-05-05 20:51 > Last updated on 2018-05-05 20:52 Consider the following example: ```text function foo(refs: Set[Ref]): Bool requires forall x: Ref :: x in refs...
> Created by **@mschwerhoff** on 2015-12-03 14:42 > Last updated on 2017-11-22 08:53 In the attached file, the package removes too many permissions to l.next.next Arguably, the reason is that...
> Created by bitbucket user **Wytse Oortwijn** on 2020-09-11 08:30 The error back-translation implementation contains a workaround for what I think might be a problem in Silver and/or Silicon. See...
> Created by **@Felalolf** on 2019-09-25 19:48 Currently, the desugarer is in a single file. This should be decomposed into multiple, more digestible files.
> Created by **@Felalolf** on 2019-10-08 15:36 > Last updated on 2020-07-07 09:09 As discussed in some Viper meeting, it seems to be a good idea to make Gobra deterministic....
> Created by **@arquintl** on 2020-06-19 07:38 > Last updated on 2020-06-19 07:44 Check that methods do not have the same name as fields This is invalid: ``` type Rectangle...
> Created by **@arquintl** on 2020-06-19 09:45 I’ve observed that the following code snippet successfully verifies with Gobra. However, in my opinion this should only work if `h` is marked...
> Created by **@Felalolf** on 2019-07-23 16:06 > Last updated on 2019-07-23 18:50 Nothhing works