viper-admin

* Update VS Code version used in tests to `1.105.1`.

Verification is taking more time than usual

7

> Created by **@fabiopakk** on 2019-07-09 15:04 > Last updated on 2020-02-11 15:46 The programs in the ‘Examples’ repository are periodically checked by the Jenkins job entitled ‘Examples Verification’. Recently...

Incompleteness when unfolding a predicate under a quantifier.

1

> Created by **@vakaras** on 2018-07-23 16:31 In the example below, the second call to `fails` fails with an error that the precondition `loc(fruits, j).val) >= 0` does not hold....

Well-definedness failures do not mask subsequent errors

2

> Created by **@alexanderjsummers** on 2017-01-09 16:44 > Last updated on 2017-01-10 14:04 In general, a failed assertion gets assumed for the subsequent verification of the current scope. However, if...

> **Pull request** :twisted_rightwards_arrows: created by **@marcoeilers** on 2017-02-07 17:57 > Original Bitbucket pull request id: 24 > > Participants: > > * **@alexanderjsummers** (reviewer) > > Source: https://github.com/viperproject/carbon/commit/097d5d6d45496f101bd205dfdf18270557dc7a54 on...

> **Pull request** :twisted_rightwards_arrows: created by bitbucket user **nadmuell** on 2016-07-12 11:31 > Last updated on 2020-01-31 20:39 > Original Bitbucket pull request id: 23 > > Participants: > >...

Unsoundness: a heap dependent function is instantiated even when its precondition does not hold

2

> Created by **@mschwerhoff** on 2019-05-08 09:12 ```plaintext function Void$discriminant(self: Ref): Int requires acc(Void(self)) ensures false { unfolding acc(Void(self)) in 8 } predicate Void(self: Ref) { false } method m_void$$unreachable$opensqu$0$closesqu$()...

Test all/assume/assume10QPwand.sil causes Boogie errors

7

> Created by **@mschwerhoff** on 2018-10-11 15:55 > Last updated on 2019-07-27 02:34 ```text java.lang.RuntimeException: missing translation for inhaling of (forall x: Ref, y: Ref, z: Ref :: { (x...

Framing of locations within predicates is not retrospective

1

> Created by **@alexanderjsummers** on 2018-10-13 12:19 In the following example, the assertions can't be proven. Adding copies of the assertions before the loop fixed the problem; the reason is...

Incompleteness: Carbon cannot prove that a memory location did not change even though it always held a predicate to it

3

> Created by **@vakaras** on 2019-06-26 15:21 > Last updated on 2019-06-26 16:04 In the following example, the last assert fails: ``` field val_int: Int predicate i32(self: Ref) { acc(self.val_int,...