viper-admin

Heap-dependent triggers are not as restrictive as expected

2

> Created by **@mschwerhoff** on 2015-12-18 08:48 > Last updated on 2019-03-08 13:56 The following example verifies in Silicon, which is sound (the assertion is actually true), but somewhat unexpected,...

Silicon instantiates axioms when trigger terms are in the wrong state

3

> Created by **@alexanderjsummers** on 2019-03-08 12:28 > Last updated on 2019-03-08 13:56 In the attached example, two methods are expected not to verify, since the trigger terms are available...

Deprecate 'new' and its semantics

1

> Created by **@alexanderjsummers** on 2018-06-29 12:09 > Last updated on 2019-03-02 22:27 We agreed at a recent Viper meeting to drop 'new' from the language, and possibly replace it...

New objects and non-aliasing information

5

> Created by **@mschwerhoff** on 2013-05-24 15:38 > Last updated on 2019-03-02 22:27 When an object is created as `v := new()`, Silicon should be able to assert that every...

Outputs differ between Silicon and Carbon

2

> Created by **@fabiopakk** on 2019-01-21 16:18 > Last updated on 2019-01-21 16:28 In the file below, the same expected output is produced by both verifier backends, **Exhale might fail**....

Unexpected verification failure with heap-dependent triggers and old

1

> Created by **@mschwerhoff** on 2018-11-25 11:50 > Last updated on 2018-11-25 12:02 The following incorrectly fails to verify in Silicon: ```text predicate P(r: Ref, x: Int) function P_state(r: Ref,...

QP domain not axiomatised for triggers

1

> Created by **@mschwerhoff** on 2018-11-24 21:41 > Last updated on 2018-11-25 11:51 I just found three occurrences of `println("domain needed")` in the code that originates from Tobias Brodmann's work...

Frame heap assumptions into read-only loops

7

> Created by **@mschwerhoff** on 2016-02-22 13:48 > Last updated on 2018-10-15 09:09 ``` #!text field f: Int method test(x: Ref) returns (a: Int) requires acc(x.f) && x.f != 0...

Mentioning recursive function body in its postcondition leads to a matching loop

3

> Created by **@vakaras** on 2018-07-25 09:14 > Last updated on 2018-08-15 10:00 The functions `fib3` and `fib4` below cause matching loops as illustrated with asserts in the methods `test3`...

bad recursive function definition not (apparently) available

3

> Created by **@alexanderjsummers** on 2018-05-08 16:03 > Last updated on 2018-06-03 10:51 Against expectations, the following assertion about an ill-defined recursive function is not proved: ``` #!scala function wild()...