"new array[]" and array.length and @MinLen

[mernst]

Consider the following code:

import java.util.List;
import org.checkerframework.common.value.qual.MinLen;

public class NewArrayLengthOf {

    String @MinLen(1) [] member_array;

    public void recurse_definitions(List<String> new_elements) {
        String[] new_array = new String[member_array.length + new_elements.size()];
        member_array = new_array;
    }
}

It should type-check, but the Index Checker issues this output:

% $ch/bin/javac -g NewArrayLengthOf.java -processor index
NewArrayLengthOf.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
        member_array = new_array;
                       ^
  found   : @UnknownVal String @UnknownVal []
  required: @UnknownVal String @ArrayLenRange(from=1, to=2147483647) []
1 error

This is most likely a Value Checker issue.

[panacekcz]

Caused by possible overflow of the addition. If member_array and new_elements have 2³² elements in total, an array of length 0 is created. Sorry, that cannot happen. However, because of the overflow, the value checker loses track of the lower bound.
Related: #182