viper-admin
viper-admin
> Created by **@fabiopakk** on 2019-02-08 17:00 After commit 3257: in Silver, some unexpected assertion errors are occurring in file wands/regression/conditionals3.sil. They were marked as unexpected output to allow a...
> Created by **@gauravpartha** on 2019-11-20 16:59 > Last updated on 2019-11-29 12:35 The translation of the Viper`predicate P(x: Ref)` leads to the following two axioms that are generated on...
> Created by **@vakaras** on 2016-12-19 14:04 > Last updated on 2017-06-19 10:02 For this program: ``` #!silver field f1: Ref field f2: Int function foo(this: Ref): Ref requires this...
> Created by **@marcoeilers** on 2017-02-14 14:52 > Last updated on 2017-05-10 18:34 The following program fails to verify; in the last line of method m, Carbon says the "precondition...
> Created by **@mschwerhoff** on 2017-01-16 13:41 The snippet predicate P(a: Ref) { acc(a.f) } ... inhale P(x) inhale forperm[P] r :: unfolding P(r) in r.f == 1 makes Carbon...
> Created by **@marcoeilers** on 2017-03-13 09:34 > Last updated on 2017-03-27 13:32 The following program leads to an exception in Carbon: ``` function f(a: Int, b: Int): Bool method...
> Created by **@alexanderjsummers** on 2017-03-26 11:01 > Last updated on 2017-03-26 11:04 In the following example, a trigger is manually specified for the select_store_diff axiom which, because of a...
> Created by **@alexanderjsummers** on 2017-05-08 17:55 It should all take place in the FuncPredModule. It's also not totally clear, but it seems as though it's currently too conservative (updating...
> Created by **@alexanderjsummers** on 2017-05-15 14:35 We need to add support for triggers on existentials. Without them, the example in Silver issue 189 fails to verify (in Carbon), since,...
> Created by **@vakaras** on 2017-05-24 14:21 This program: ``` #!silver field val: Int method test() { package true --* (forall n: Ref :: acc(n.val)) } ``` causes the following...