Arrays.copyOf should propagate length information from argument to return value

[mernst]

Consider this source code.

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

public class ArraysCopyOfLength {

  public static void m1(String @MinLen(1) [] args) {
    String @MinLen(1) [] args2 = Arrays.copyOf(args, args.length);
  }

  public static void m2(String @MinLen(1) ... args) {
    String @MinLen(1) [] args2 = Arrays.copyOf(args, args.length);
  }
}

The Index Checker issues these warnings:

ArraysCopyOfLength.java:7: error: [assignment.type.incompatible] incompatible types in assignment.
    String @MinLen(1) [] args2 = Arrays.copyOf(args, args.length);
                                              ^
  found   : @UnknownVal String @UnknownVal []
  required: @UnknownVal String @ArrayLenRange(from=1, to=2147483647) []
ArraysCopyOfLength.java:11: error: [assignment.type.incompatible] incompatible types in assignment.
    String @MinLen(1) [] args2 = Arrays.copyOf(args, args.length);
                                              ^
  found   : @UnknownVal String @UnknownVal []
  required: @UnknownVal String @ArrayLenRange(from=1, to=2147483647) []
2 errors

However, these are false positive warnings, because the result of these calls to Arrays.copyOf should have all the same properties as its argument.