blob: 0726e3498e76bca903c64e7716f929b94564e1fc (
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(read3);
{
unfold rd(read3); // ERROR: scaling epsilons is not possible
}
}
|
