| import org.checkerframework.checker.index.qual.GTENegativeOne; |
| import org.checkerframework.checker.index.qual.NonNegative; |
| import org.checkerframework.checker.index.qual.Positive; |
| |
| public class TransferSub { |
| |
| void test() { |
| // zero, one, and two |
| int a = 1; |
| |
| @NonNegative int b = a - 1; |
| // :: error: (assignment) |
| @Positive int c = a - 1; |
| @GTENegativeOne int d = a - 2; |
| |
| // :: error: (assignment) |
| @NonNegative int e = a - 2; |
| |
| @GTENegativeOne int f = b - 1; |
| // :: error: (assignment) |
| @NonNegative int g = b - 1; |
| |
| // :: error: (assignment) |
| @GTENegativeOne int h = f - 1; |
| |
| @GTENegativeOne int i = f - 0; |
| @NonNegative int j = b - 0; |
| @Positive int k = a - 0; |
| |
| // :: error: (assignment) |
| @Positive int l = j - 0; |
| // :: error: (assignment) |
| @NonNegative int m = i - 0; |
| |
| // :: error: (assignment) |
| @Positive int n = a - k; |
| // this would be an error if the values of b and j (both zero) weren't known at compile time |
| @NonNegative int o = b - j; |
| /* i and d both have compile time value -1, so this is legal. |
| The general case of GTEN1 - GTEN1 is not, though. */ |
| @GTENegativeOne int p = i - d; |
| |
| // decrements |
| |
| // :: error: (unary.decrement) :: error: (assignment) |
| @Positive int q = --k; // k = 0 |
| |
| // :: error: (unary.decrement) |
| @NonNegative int r = k--; // after this k = -1 |
| |
| int k1 = 0; |
| @NonNegative int s = k1--; |
| |
| // :: error: (assignment) |
| @NonNegative int s1 = k1; |
| |
| // transferred to SimpleTransferSub.java |
| // this section is failing due to CF bug |
| // int k2 = 0; |
| // // :: error: (assignment) |
| // @Positive int s2 = k2--; |
| |
| k1 = 1; |
| @NonNegative int t = --k1; |
| |
| k1 = 1; |
| // :: error: (assignment) |
| @Positive int t1 = --k1; |
| |
| int u1 = -1; |
| @GTENegativeOne int x = u1--; |
| // :: error: (assignment) |
| @GTENegativeOne int x1 = u1; |
| } |
| } |
| // a comment |