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
|
package fieldinvar;
import org.checkerframework.common.value.qual.BottomVal;
import org.checkerframework.common.value.qual.MinLen;
import org.checkerframework.common.value.qual.MinLenFieldInvariant;
import org.checkerframework.framework.qual.FieldInvariant;
public class MinLenFieldInvar {
class Super {
public final int @MinLen(2) [] minlen2;
public Super(int @MinLen(2) [] minlen2) {
this.minlen2 = minlen2;
}
}
// :: error: (field.invariant.not.subtype)
@MinLenFieldInvariant(field = "minlen2", minLen = 1)
class InvalidSub extends Super {
public InvalidSub() {
super(new int[] {1, 2});
}
}
@MinLenFieldInvariant(field = "minlen2", minLen = 4)
class ValidSub extends Super {
public final int[] validSubField;
public ValidSub(int[] validSubField) {
super(new int[] {1, 2, 3, 4});
this.validSubField = validSubField;
}
}
// :: error: (field.invariant.not.found.superclass)
@MinLenFieldInvariant(field = "validSubField", minLen = 3)
class InvalidSubSub1 extends ValidSub {
public InvalidSubSub1() {
super(new int[] {1, 2});
}
}
// :: error: (field.invariant.not.subtype.superclass)
@MinLenFieldInvariant(field = "minlen2", minLen = 3)
class InvalidSubSub2 extends ValidSub {
public InvalidSubSub2() {
super(new int[] {1, 2});
}
}
@FieldInvariant(field = "minlen2", qualifier = BottomVal.class)
@MinLenFieldInvariant(field = "validSubField", minLen = 4)
class ValidSubSub extends ValidSub {
public ValidSubSub() {
super(null);
}
void test() {
int @BottomVal [] bot = minlen2;
int @MinLen(4) [] four = validSubField;
}
}
}
|
