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
|
import org.checkerframework.common.value.qual.ArrayLen;
import org.checkerframework.common.value.qual.ArrayLenRange;
import org.checkerframework.common.value.qual.StringVal;
class StringLenRefinement {
void refineLenRange(
@ArrayLenRange(from = 3, to = 10) String range,
@ArrayLen({4, 6, 12}) String lens,
@StringVal({"aaaa", "bbbb", "cccccc", "dddddddddddd"}) String vals) {
if (range.length() <= 7) {
@ArrayLenRange(from = 3, to = 7) String shortRange = range;
} else {
@ArrayLenRange(from = 8, to = 10) String longRange = range;
}
if (lens.length() <= 7) {
@ArrayLen({4, 6}) String shortLens = lens;
} else {
@ArrayLen({12}) String longLens = lens;
}
if (vals.length() <= 7) {
@StringVal({"aaaa", "bbbb", "cccccc"}) String shortVals = vals;
} else {
@StringVal({"dddddddddddd"}) String longVals = vals;
}
}
void refineLen(
@ArrayLenRange(from = 3, to = 10) String range, @ArrayLen({4, 8, 12}) String lens) {
if (range.length() == 5 || range.length() == 8 || range.length() == 13) {
@ArrayLen({5, 8}) String refinedArg = range;
}
if (lens.length() == 5 || lens.length() == 8 || lens.length() == 13) {
@ArrayLen({8}) String refinedLens = lens;
}
}
}
|
