viper-admin

Finding predicates with arguments in the heap

6

> Created by **@mschwerhoff** on 2013-07-25 10:23 > Last updated on 2017-09-23 13:47 As illustrated by the test file `Sil:all/predicates/arguments.sil`, Silicon isn't able to verify snippets such as inhale acc(this.valid(b),...

Disjunctive aliasing constraints and permissions

17

> Created by bitbucket user **Korbinian Breu** on 2014-02-21 09:11 > Last updated on 2017-09-23 13:45 ``` #!scala method foo2(s: Seq[Ref]) requires |s| > 2 && acc(s[0].f, write) && acc(s[1].f,...

Exhale acc(P(x), perm(P(x))) can fail surprisingly due to disjunctive aliasing constraints

6

> Created by **@vakaras** on 2016-04-10 17:08 > Last updated on 2017-09-23 13:47 The minimal example: ``` #!Silver predicate obligationGenerationGuard$(r$: Ref) { true } method test(c: Ref, d: Ref, e:...

Replace "Verification Aborted Exceptionally" and "Unknown Reason"/loglevel-related messages with more-specific messages

1

> Created by **@alexanderjsummers** on 2017-09-08 14:03 > Last updated on 2017-09-25 10:25 The exceptional error messages sometimes produced by Silicon are hard to debug, particularly from the IDE. For...

Incompleteness from non-linear (permission) arithmetic

9

> Created by bitbucket user **fhahn** on 2015-11-19 10:10 > Last updated on 2019-08-28 21:03 Silicon seems to have problems unfolding predicates with variable permission parameter. For the following listing...

Silicon hangs if smt code sent to Z3 isn't indented

2

> Created by **@alexanderjsummers** on 2015-06-04 09:54 Silicon requires that multi-line constructs (such as axioms) be indented, such that only the first line is without an indent. If modifying e.g....

Silicon generates invalid SMT code ("unknown constant") for QPs in functions

6

> Created by bitbucket user **gishors** on 2018-04-04 07:13 > Last updated on 2019-05-08 14:00 _**Important**:_ This issue's cause roots in quantified permissions. If you get `"unknown constant"`/\`"unknown function"\` errors...

Don't warn about unresolved expressions in functions if they are unreachable/dead code

11

> Created by **@marcoeilers** on 2016-12-13 21:26 > Last updated on 2018-08-26 09:54 For functions containing unreachable expressions, like the following: ``` function f(): Int { (true ? f1() :...

Make sequence axiomatisation common with Carbon

4

> Created by **@alexanderjsummers** on 2014-07-14 12:34 > Last updated on 2020-02-03 13:32 We should find a way to make the two verifiers use the same file for sequence, set...

Missing axiom(s) in the axiomatization of sets

5

> Created by bitbucket user **OmerSakar** on 2019-12-13 15:25 > Last updated on 2019-12-13 15:52 When reasoning about a set and its subset \(using the subset operator\), there seems to...