viper-admin

examples\list_insert_tmp.sil doesn't verify

1

> Created by **@fabiopakk** on 2019-11-18 14:01 > Last updated on 2019-11-18 14:12 Similarly to issue viperproject/silicon~~~~ in Silicon, Carbon is also failing at the same line with the same...

> Created by **@alexanderjsummers** on 2020-01-01 23:31 See issues/silicon/0400.vpr ‌ --- Attachments: * [**`0400.vpr`**](https://gist.githubusercontent.com/viper-admin/dcf3d95f5b232a7e1f017206cb7c3289/raw/499454ebdd1f31733df26db04f7a33952f0be3b2/0400.vpr)

> Created by **@alexanderjsummers** on 2020-01-02 00:26 `(forall i: Int :: i == 0 ==> acc(P(), write) --* acc(Q(0), write))` doesn’t have a case for inhaling: ``` [info] java.lang.RuntimeException: missing...

Make sequence axiomatisation common with Silicon

2

> Created by **@fabiopakk** on 2020-02-03 13:30 We should find a way to make the two verifiers use the same file for sequence, set axioms etc. to avoid diverging fixes....

Heap-dependent triggers not yet fully supported

3

> Created by **@mschwerhoff** on 2018-10-12 13:46 > Last updated on 2020-02-14 14:41 Affects at least test case `all/heap-dependent_triggers/heapTriggersInhaleExhale.sil`, but probably also tests ignored due to , e.g. `all/heap-dependent_triggers/triggerFoldPackage.sil` and...

> Created by bitbucket user **OmerSakar** on 2019-12-13 15:25 When reasoning about a set and its subset \(using the subset operator\), there seems to be an axiom missing that relates...

Unexpected output in examples repository

2

> Created by **@fabiopakk** on 2019-03-12 13:51 > Last updated on 2019-11-04 15:05 This is a container of all issues related to unexpected outputs in `examples` repository, produced by Carbon....

Incoherent loop treatment (scoping)

2

> Created by bitbucket user **Thibault Dardinier** on 2019-10-30 09:56 > Last updated on 2019-10-30 10:45 ‌ ``` field f: Int method works(x: Ref) requires acc(x.f) { x.f := 5...

Exhaling field permissions fails after unfolding a predicate with permissions returned by `perm()`

8

> Created by bitbucket user **fhahn** on 2015-12-07 16:48 > Last updated on 2019-10-30 10:33 The following program fails when trying to `exhale acc(x.Foo__a)`, even though the assertion `perm(x.Foo__a) >...

interaction between wildcard permissions and quantified permissions is unreliable

1

> Created by **@alexanderjsummers** on 2016-01-14 10:38 > Last updated on 2019-08-28 13:10 Some test cases work, but quantifiedpermissions/issues/issue_0096.sil and quantifiedpermissions/sets/unionfind.sil cause [info] java.lang.RuntimeException: cannot translate wildcard at an arbitrary...