Rely-guarantee invariants are not supported in Chalice2Silver

[viper-admin]

Created by bitbucket user ykass on 2014-08-26 13:14 Last updated on 2015-07-07 11:03

The occurrence of "old" in an invariant triggers a "not well-formed predicate" error by Silicon.

[viper-admin]

@vakaras commented on 2015-07-07 11:03

Example code:

#!Chalice

class Counter1 {
  var x: int;
  // Should be rejected because invariant is not reflexive.
  invariant acc(x) && old(x) < x;
}

class Counter2 {
  var x: int;
  // Should work.
  invariant acc(x) && old(x) <= x;
}