viper-admin

Test all/assume/assume10QPpred.sil causes Boogie errors

1

> Created by **@mschwerhoff** on 2018-10-12 13:31 > Last updated on 2019-08-28 13:03 ```text all/assume/assume10QPpred.sil [carbon-Silver] *** FAILED *** (1 second, 219 milliseconds) 13 errors The following output occurred during...

Heap dependent triggers are instantiating more than expected

1

> Created by **@alexanderjsummers** on 2019-08-16 15:49 > Last updated on 2019-08-19 13:15 Heap dependent triggers test file seems to observe more instantiations than expected, causing the following test to...

Incompleteness when unrolling a loop too many times

3

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

Sequence-related incompletenesses

1

> Created by **@alexanderjsummers** on 2019-05-16 13:36 > Last updated on 2019-05-16 13:37 This is a catch-all issue for observable incompletenesses in the sequence axiomatisation. Since I started upgrading the...

Carbon crashes for ill-formed command line options

3

> Created by **@mueller55** on 2016-06-23 10:05 > Last updated on 2019-03-11 09:12 It crashes basically whenever the options are wrong: * unknown option * missing argument to an option...

Some of the expected output isn't occurring in Carbon

3

> Created by **@fabiopakk** on 2019-01-21 16:02 > Last updated on 2019-02-04 08:58 In the **examples** repository, in directory **verifythis-exercises**, the expected output is not occurring in Carbon, only in...

Set and sequence combinations are not always handled automatically

4

> Created by **@alexanderjsummers** on 2016-02-24 17:44 > Last updated on 2018-07-06 14:06 This can be particularly relevant for quantified permissions. See, for example, quantifiedpermissions/issues/issue_0064.sil This is ultimately concerned with...

> Created by **@alexanderjsummers** on 2018-06-29 12:10 We agreed at a recent Viper meeting to drop 'new' from the language, and possibly replace it with 'havoc'. I suggest that, in...

> Created by bitbucket user **brotobia** on 2018-06-21 08:04 * Support using magic wands inside perm expressions * Support using general predicates and magic wands in forperm expressions

Examples without proper triggers don't verify

2

> Created by **@alexanderjsummers** on 2016-01-13 17:09 > Last updated on 2018-06-09 12:08 Because of a lack of appropriate triggers (at least for composite.sil), the examples composite.sil and bsearch.sil don't...