false positive in @NonNegative check #7008
Description
final int referenceIndex = extractReferencePart(content);
Optional<JavadocTag> validTag = Optional.empty();
if (referenceIndex != -1) {
final String referenceString;
if (referenceIndex == 0) {
referenceString = content;
}
else {
referenceString = content.substring(0, referenceIndex);
}
The Checker Framework incorrectly reports an error for content.substring(0, referenceIndex), stating that referenceIndex must be a @nonnegative int. However, the condition if (referenceIndex != -1) ensures that only possible negative return value is handled before execution.
Is there a way for Checker Framework to handle this inference internally and recognize the safety of referenceIndex?
<message>incompatible argument for parameter endIndex of String.substring.</message>
<lineContent>referenceString = content.substring(0, referenceIndex);</lineContent>
<details>
found : int
required: @NonNegative int
</details>