viper-admin

A heap-dependent function can lead to a matching loop without any explicit quantifiers

5

> Created by **@vakaras** on 2018-07-25 09:06 > Last updated on 2018-08-15 11:30 The function `fib2` below causes a matching loop as illustrated with an assert in the method `test2`...

Inhale-exhale assertions unsound if used in functions or predicates

4

> Created by **@mschwerhoff** on 2017-03-01 10:45 > Last updated on 2019-08-28 10:07 Silicon's current way of representing the footprints of functions and predicates is unsound in combination with inhale-exhale...

> Created by **@mschwerhoff** on 2017-09-25 09:03 The current implementation of magic wand snapshots can result in contradicting assumptions (i.e. is unsound) if a magic wand (chunk) is applied more...

Verification fails with java.util.NoSuchElementException: head of empty list

11

> Created by **@fpoli** on 2018-05-31 16:31 > Last updated on 2019-07-29 14:43 The attached program passes the consistency checks, but causes a `java.util.NoSuchElementException: head of empty list` during the...

Permission incompletenesses

9

> Created by **@mschwerhoff** on 2013-04-15 07:14 > Last updated on 2017-09-23 13:41 The separation of the symbolic state into a heap and path conditions entails permission-related incompletenesses of various...

Function postconditions available too late

2

> Created by **@marcoeilers** on 2018-09-26 10:26 > Last updated on 2019-07-23 17:02 The order in which Silicon verifies functions (and their definitions therefore become available) does not take into...

Incompleteness when unrolling a loop too many times

11

> Created by bitbucket user **robinsierra** on 2019-06-04 17:45 > Last updated on 2019-07-29 12:58 When doing loop unrolling both Silicon and Carbon hit a limit after which they can’t...

Cannot prove properties of multiset intersection

1

``` method test06(B: Multiset[Int], n: Int, x: Int) requires |B| == n { var B1: Multiset[Int] := B intersection B assert |B1| == n // fails assert B1 == B...

Matrix Addition example (encoded via domains) does not verify

6

> Created by **@alexanderjsummers** on 2017-05-08 10:33 > Last updated on 2018-06-09 12:16 See the attached file - the first loop invariant cannot be shown to be preserved --- Attachments:...

Non-aliasing assumptions from unfolding predicates

5

> Created by **@mschwerhoff** on 2013-07-31 08:48 > Last updated on 2019-11-16 14:58 Additional non-aliasing assumptions could be generated when unfolding permissions, as illustrated by the following program: ``` field...