viper-admin

Trigger generation may generate triggers which don't work at call site

2

> Created by **@alexanderjsummers** on 2016-10-18 17:53 > Last updated on 2016-10-18 18:04 Trigger generation for quantifiers occurring in e.g. method contracts will decide which terms are valid in triggers...

> Created by **@mschwerhoff** on 2016-09-27 07:25 For example, the following `import` statements fail: import ".\foo.vpr" // Can be rewritten to "./foo.vpr" import "D:\Temp\test153.sil" // Not sure if an absolute...

> Created by bitbucket user **a_helfenstein** on 2016-06-21 15:32 It would be nice to have a test annotation for running the test case with some specific command line option for...

Sequence-related incompleteness, potentially trigger-related

1

> Created by **@mschwerhoff** on 2016-02-15 20:15 > Last updated on 2016-02-15 22:23 The postcondition of `test02` fails in Silicon and Carbon if the assertion in the body is commented....

> Created by **@mschwerhoff** on 2016-01-13 13:17 ``` #!text method test01(xs: Set[Int], ys: Set[Int], z: Int) { inhale |xs intersection ys| == 0 inhale |xs intersection Set(z)| == 0 exhale...

* Updates ViperServer from `2f7124f970487c7faead97723269e373d49a2c6c` to `7b4d0d1c401b985537a4a3ae502f39a8fe5ac7fa`.

* Updates ViperServer from `7b4d0d1c401b985537a4a3ae502f39a8fe5ac7fa` to `00a0782b225b258aa7797063b1c868499081a32e`.