viper-admin
viper-admin
> Created by **@alexanderjsummers** on 2018-06-05 16:14 > Last updated on 2018-06-06 09:42 The existing code selects triggers slightly differently on inhale and on exhale. In addition (as commented in...
> Created by **@MartinClochard** on 2018-05-16 12:32 In the attached example, the freshly created location cannot be verified to be outside the input set, even though this would lead to...
> Created by **@MartinClochard** on 2018-05-08 15:17 > Last updated on 2018-05-09 15:42 Against expectations, the following assertion about an ill-defined recursive function is not proved: ``` #!scala function wild()...
> Created by **@alexanderjsummers** on 2018-04-28 12:37 > Last updated on 2018-04-28 12:43 We should add these checks to both backends. The tests have also been added to sequences/sequences.sil ```...
> Created by **@vakaras** on 2018-03-30 18:02 The following example succeeds in Silicon but fails in Carbon: ``` #!silver field x: Ref field y: Ref function globalRd(): Perm ensures none...
> Created by **@aterga** on 2018-03-01 16:08 The problem seems to be related to triggering. The QP body doesn't get triggered when new an object is created via ```new``` expressions:...
> Created by **@aterga** on 2018-01-23 16:31 > Last updated on 2018-01-23 17:02 The following example should verify (according to the way we understand Viper programs): ```Viper method m1(){ assert...
> Created by **@fpoli** on 2018-08-15 15:29 > Last updated on 2018-08-15 15:35 Why there is no `folding ... in ...` expression? * It's the dual of `unfolding`, which exists;...
> Created by **@mschwerhoff** on 2015-06-10 07:25 > Last updated on 2019-05-16 13:37 ``` #!text method m03(S1: Seq[Ref], S2: Set[Ref], x: Ref) requires S1 == Seq(x) && S2 == Set(x)...
> Created by bitbucket user **robinsierra** on 2019-11-05 13:29 > Last updated on 2020-02-06 13:09 The two backends produce different behavior for division. The following Viper program verifies in Silicon...