Chalice/tests/predicates/aux-info.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

class Cell {
  var value: int;
  
  predicate p { acc(value,1) }
  
  method test()
    requires p && acc(value,2)
  {
    // previously, the following sequence let to negative secondary permission
    // to the field value.
    fold p
    fold p
    call void()
    call void()
    call void2()
    
    unfold p
    var tmp: int := value
    fold p
    // make sure that at this point we can retain information about the field value
    assert tmp == unfolding p in value // ERROR: currently, Chalice cannot prove this, which it should be able to do
  }
  
  method void()
    requires p
  {}
  
  method void2()
    requires p
    ensures p
  {}
  
}