Function nextToken

parser.go:226–237

SYS-REQ-001 Find position of next character which is not whitespace reqproof:lemma nextToken_in_range func(data []byte) bool { r := nextToken(data) return r >= -1 && r < len(data) } reqproof:lemma nextToken_empty_neg func(data []byte) bool { return !(len(data) == 0) || nextToken(data)

(data []byte)

//	  return true
//	}
func nextToken(data []byte) int {
	for i, c := range data {
		// reqproof:invariant 0 <= i
		// reqproof:invariant i <= len(data)
		if c == ' ' || c == '\n' || c == '\r' || c == '\t' {
			continue
		}
		return i
	}

	return -1
}

// SYS-REQ-001
// Find position of last character which is not whitespace