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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
import org.checkerframework.common.value.qual.*;
public class TransferSub {
void test() {
// zero, one, and two
int a = 1;
@IntRange(from = 0) int b = a - 1;
// :: error: (assignment.type.incompatible)
@IntRange(from = 1) int c = a - 1;
@IntRange(from = -1) int d = a - 2;
// :: error: (assignment.type.incompatible)
@IntRange(from = 0) int e = a - 2;
@IntRange(from = -1) int f = b - 1;
// :: error: (assignment.type.incompatible)
@IntRange(from = 0) int g = b - 1;
// :: error: (assignment.type.incompatible)
@IntRange(from = -1) int h = f - 1;
@IntRange(from = -1) int i = f - 0;
@IntRange(from = 0) int j = b - 0;
@IntRange(from = 1) int k = a - 0;
// :: error: (assignment.type.incompatible)
@IntRange(from = 1) int l = j - 0;
// :: error: (assignment.type.incompatible)
@IntRange(from = 0) int m = i - 0;
// :: error: (assignment.type.incompatible)
@IntRange(from = 1) int n = a - k;
// this would be an error if the values of b and j (both zero) weren't known at compile time
@IntRange(from = 0) int o = b - j;
/* i and d both have compile time value -1, so this is legal.
The general case of GTEN1 - GTEN1 is not, though. */
@IntRange(from = -1) int p = i - d;
// decrements
// :: error: (unary.decrement.type.incompatible)
// :: error: (assignment.type.incompatible)
@IntRange(from = 1) int q = --k; // k = 0
// :: error: (unary.decrement.type.incompatible)
@IntRange(from = 0) int r = k--; // after this k = -1
int k1 = 0;
@IntRange(from = 0) int s = k1--;
// :: error: (assignment.type.incompatible)
@IntRange(from = 0) int s1 = k1;
k1 = 1;
@IntRange(from = 0) int t = --k1;
k1 = 1;
// :: error: (assignment.type.incompatible)
@IntRange(from = 1) int t1 = --k1;
int u1 = -1;
@IntRange(from = -1) int x = u1--;
// :: error: (assignment.type.incompatible)
@IntRange(from = -1) int x1 = u1;
}
}
|
