Infer MinLen(1) after checking !isEmpty()

[panacekcz]

After checking that !s.isEmpty(), s can be @MinLen(1).

Code:

import org.checkerframework.common.value.qual.MinLen;

public class IsEmptyMinLen {
    public void m1(String s) {
        if(!s.isEmpty()) {
            char c = s.charAt(0);           
        }
    }

    public void m2(String s) {
        if(!s.isEmpty()) {
            @MinLen(1) String t = s;            
        }
    }
}

Output:

IsEmptyMinLen.java:6: error: [argument.type.incompatible] incompatible types in argument.
            char c = s.charAt(0);           
                              ^
  found   : @UpperBoundUnknown int
  required: @LTLengthOf(value="s", offset={}) int
IsEmptyMinLen.java:12: error: [assignment.type.incompatible] incompatible types in assignment.
            @MinLen(1) String t = s;            
                                  ^
  found   : @UnknownVal String
  required: @ArrayLenRange(from=1, to=2147483647) String
2 errors

[panacekcz]

Closed in favor of kelloggm#201