void (char buffer[], int startOffset, int length) { if (startOffset < 0 || startOffset > buffer.length || length < 0 || startOffset + length > buffer.length || startOffset + length < 0) { throw new IndexOutOfBoundsException(); } // This is always false, but we cannot reliably detect this yet. If startOffset == buffer.length // then startOffset + length <= buffer.length implies that length == 0 *or* startOffset + length overflows // The latest case is ruled out by startOffset + length < 0, but our memory state is unable to track this. if (startOffset == buffer.length && length > 0) { } }