viper-admin
viper-admin
> Created by **@vakaras** on 2018-03-18 19:38 > Last updated on 2018-03-19 12:54 Example: ``` #!silver method test() ensures ( true --* let tmp2 == ( true ) in (...
> Created by **@marcoeilers** on 2017-06-28 13:36 > Last updated on 2017-11-27 14:28 Silver currently interprets "/" as a division resulting in a permission, and "\" as integer division. Since...
> Created by **@aterga** on 2016-04-10 02:53 > Last updated on 2017-11-26 16:44 The error could be reproduced if the following multi-file Silver program starts from either liba.sil or libb.sil....
> Created by **@mschwerhoff** on 2016-04-08 10:07 > Last updated on 2017-11-26 15:34 A common mistake is writing var x: Ref := new(*) which is not allowed since `x :=...
> Created by bitbucket user **juhaszu** on 2014-11-03 11:14 > Last updated on 2017-11-26 14:45 Currently we report a type error using the first character of the offending expression. This...
> Created by **@aterga** on 2017-10-05 14:38 The method ```readableMessage``` is overridden in many implementations of ```AbstractError```. Sometimes is takes two parameters, such as ```Scala def readableMessage(withId: Boolean = false,...
> Created by **@mueller55** on 2016-11-22 14:15 > Last updated on 2017-06-28 15:24 We should provide a smoke detector to make it easier to detect if an encoding is unsound....
> Created by **@mschwerhoff** on 2017-06-11 21:05 > Last updated on 2017-06-25 17:08 Carbon and Silicon currently differ in their handling of (un)folding a wildcard fraction of a predicate. Consider...
> Created by **@mschwerhoff** on 2017-04-20 12:15 Currently, Viper rejects assertions that nest `perm` under `forperm`, e.g. forperm[f] r :: perm(r.f) == write ==> true However, there doesn't seem to...
> Created by **@mschwerhoff** on 2017-04-19 13:48 Unit test `silver/src/test/scala/DomainInstanceTest.scala` includes a check that, for a given Viper file, 259 domain instances should be computed. However, on some runs, 278...