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
|
import org.checkerframework.common.value.qual.IntRange;
import org.checkerframework.common.value.qual.IntVal;
public class MathMinMax {
void mathTest1(@IntRange(from = 0, to = 10) int x, @IntRange(from = 5, to = 15) int y) {
@IntRange(from = 0, to = 10) int min = Math.min(x, y);
@IntRange(from = 5, to = 15) int max = Math.max(x, y);
}
void mathTest2(@IntRange(from = 0, to = 10) int x, @IntRange(from = 11, to = 15) int y) {
@IntRange(from = 0, to = 10) int min = Math.min(x, y);
@IntRange(from = 11, to = 15) int max = Math.max(x, y);
}
void mathTest3(@IntRange(from = 0, to = 20) int x, @IntRange(from = 5, to = 15) int y) {
@IntRange(from = 0, to = 15) int min = Math.min(x, y);
@IntRange(from = 5, to = 20) int max = Math.max(x, y);
@IntVal(1) int minConst = Math.min(1, 2);
@IntVal(2) int maxConst = Math.max(-1, 2);
}
void mathTest(long x, long y) {
long min = Math.min(x, y);
long max = Math.max(x, y);
}
void mathTest(double x, double y) {
double min = Math.min(x, y);
double max = Math.max(x, y);
}
void mathTetMax(@IntRange int x, @IntRange int y) {
@IntRange int z = Math.min(x, y);
}
}
|
