| import org.checkerframework.common.value.qual.ArrayLen; |
| import org.checkerframework.common.value.qual.ArrayLenRange; |
| import org.checkerframework.common.value.qual.StringVal; |
| |
| public 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; |
| } |
| } |
| } |
