Function tokenStart

parser.go:187–199

SYS-REQ-001 reqproof:lemma tokenStart_in_range func(data []byte) bool { r := tokenStart(data) return r >= 0 && r <= len(data) } reqproof:lemma tokenStart_nonneg func(data []byte) bool { return tokenStart(data) >= 0 } reqproof:lemma tokenStart_empty_zero func(data []byte) bool { r

(data []byte)

//	  return r == 0
//	}
func tokenStart(data []byte) int {
	for i := len(data) - 1; i >= 0; i-- {
		// reqproof:invariant -1 <= i
		// reqproof:invariant i < len(data)
		c := data[i]
		if c != 10 && c != 13 && c != 9 && c != 44 && c != 123 && c != 91 {
			continue
		}
		return i
	}

	return 0
}

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