Function lastToken

parser.go:279–291

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

(data []byte)

//	  return true
//	}
func lastToken(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 == ' ' || c == '\n' || c == '\r' || c == '\t' {
			continue
		}
		return i
	}

	return -1
}

// SYS-REQ-045
// Tries to find the end of string