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 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
|
import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.Positive;
public class TransferAdd {
void test() {
// adding zero and one and two
int a = -1;
@Positive int a1 = a + 2;
@NonNegative int b = a + 1;
@NonNegative int c = 1 + a;
@GTENegativeOne int d = a + 0;
@GTENegativeOne int e = 0 + a;
// :: error: (assignment.type.incompatible)
@Positive int f = a + 1;
@NonNegative int g = b + 0;
@Positive int h = b + 1;
@Positive int i = h + 1;
@Positive int j = h + 0;
// adding values
@Positive int k = i + j;
// :: error: (assignment.type.incompatible)
@Positive int l = b + c;
// :: error: (assignment.type.incompatible)
@Positive int m = d + c;
// :: error: (assignment.type.incompatible)
@Positive int n = d + e;
@Positive int o = h + g;
// :: error: (assignment.type.incompatible)
@Positive int p = h + d;
@NonNegative int q = b + c;
// :: error: (assignment.type.incompatible)
@NonNegative int r = q + d;
@NonNegative int s = k + d;
@GTENegativeOne int t = s + d;
// increments
// :: error: (assignment.type.incompatible)
@Positive int u = b++;
@Positive int u1 = b;
@Positive int v = ++c;
@Positive int v1 = c;
int n1p1 = -1, n1p2 = -1;
@NonNegative int w = ++n1p1;
@NonNegative int w1 = n1p1;
// :: error: (assignment.type.incompatible)
@Positive int w2 = n1p1;
// :: error: (assignment.type.incompatible)
@Positive int w3 = n1p1++;
// :: error: (assignment.type.incompatible)
@NonNegative int x = n1p2++;
@NonNegative int x1 = n1p2;
// :: error: (assignment.type.incompatible)
@Positive int y = ++d;
// :: error: (assignment.type.incompatible)
@Positive int z = e++;
}
}
// a comment
|