Function tokenEnd

parser.go:55–66

SYS-REQ-044 reqproof:lemma tokenEnd_in_range func(data []byte) bool { r := tokenEnd(data) return r >= 0 && r <= len(data) } reqproof:lemma tokenEnd_nonneg func(data []byte) bool { // tokenEnd never signals via a negative sentinel — the empty-input // path returns len(data)==0 (still

(data []byte)

//	  return true
//	}
func tokenEnd(data []byte) int {
	for i, c := range data {
		// reqproof:invariant 0 <= i
		// reqproof:invariant i <= len(data)
		if c != 32 && c != 10 && c != 13 && c != 9 && c != 44 && c != 125 && c != 93 {
			continue
		}
		return i
	}

	return len(data)
}

// isJSONWhitespace reports whether b is one of the four JSON whitespace bytes
// (space 0x20, tab 0x09, LF 0x0A, CR 0x0D) per RFC 8259 §2. Used by Delete's