blob: cc8d7d285e05f691783cb7c54524b5e12c8fea24 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
class Cell {
var x: int;
// --- some predicates ---
predicate write1 { acc(x) } // full permission in a predicate
predicate write2 { acc(x,10) } // 10%
predicate read1 { rd(x) } // fractional read permission
predicate read2 { rd*(x) } // starred fractional read permission
predicate read3 { rd(x,1) } // counting permission (1 epsilon)
// --- invalid permission scaling ---
method error()
requires rd(read1,1);
{
unfold rd(read1,1); // ERROR: scaling epsilons is not possible
}
}
|
