Length cannot be stored as unsigned

[gokaco]

This error has come repeatedly in case studies where length was used as unsigned but due to weakness in signedness checker, we had to suppress the error.
Command-

javac -processor signedness ex.java

Code-

import org.checkerframework.checker.signedness.qual.*;
class ex{
	void foo(String a,byte []b){
		@Unsigned int len = a.length();
		@Unsigned int len2 = b.length;
	}
}

Output-

ex.java:4: error: [assignment.type.incompatible] incompatible types in assignment.
		@Unsigned int len = a.length();
		                            ^
  found   : @Signed int
  required: @Unsigned int
ex.java:5: error: [assignment.type.incompatible] incompatible types in assignment.
		@Unsigned int len2 = b.length;
		                      ^
  found   : @Signed int
  required: @Unsigned int
2 errors
`

[mernst]

More generally, @NonNegative int should be treated as @Constant (which will later be renamed to @SignednessEither).

[mernst]

The Signedness Checker reads annotations from the Value Checker, such as @IntRange.

If the Value Checker properly handles a.length and s.length(), I would expect the Signedness Checker should too.

So there are two things to verify:

• The Value Checker handles the length method and field.
• The Signedness Checker reads the Value Checker annotations.

Note that array.length is (or should be) special-cased by the Value Checker, because there is nowhere to write a JDK annotation.

[gokaco]

Fixed through #2614