@LessThan treatment of & bitwise mask operation

[Maxi17]

Consider this snippet:

import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.common.value.qual.IntRange;

public class Testing {

    private static @IntRange(from = 0, to = 63) int firstNumber;

    private static void method() {
        @LessThan("this.firstNumber") int secondNumber = firstNumber & 7; // Error here
        firstNumber -= secondNumber; // Error here
    }
}

Running javac -processor org.checkerframework.checker.index.IndexChecker Testing.java issues two errors:

Error:(10, 83) java: [assignment.type.incompatible] incompatible types in assignment.
  found   : @LessThanUnknown int
  required: @LessThan("Testing.firstNumber") int

Error:(11, 21) java: [compound.assignment.type.incompatible] incompatible result type in compound assignment.
  found   : @UnknownVal int
  required: @IntRange(from=0, to=63) int

The first error tells that the checker doesn't know that 'firstNumber & 7' is less than 'firstNumber' (or equal). Note that for non-negative numbers, (number & 7) is the same as (number % 8). Changing @IntRange(from = 0, to = 63) ---> @IntRange(from = 1, to = 63), the first error disappears. Now consider the following snippet:

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.common.value.qual.ArrayLen;

public class Testing {

    private static int @ArrayLen(64) [] array;

    private static @IndexFor("this.array") int firstNumber;

    private static void method() {
        @LessThan("this.firstNumber") int secondNumber = firstNumber & 7; // Error here
        firstNumber -= secondNumber;
    }
}

The only difference is that firstNumber is annotated with @IndexFor, pointing to an array with 64 elements. It should take the same values as before (@IntRange(from = 0, to = 63)). However, the second error disappears. Maybe that's because the checker can't make the connection between @IntRange() and @IndexFor() correctly.

[smillst]

The LessThan Checker is very simple and is only intended to support the Index Checker. This is one way it could be improved.