Function h2I

escape.go:60–71

reqproof:lemma h2I_range func(c byte) bool { r := h2I(c) return r == -1 || (r >= 0 && r <= 15) } reqproof:lemma h2I_decimal_digit func(c byte) bool { if c < '0' || c > '9' { return true } r := h2I(c) return r >= 0 && r <= 9 } reqproof:lemma h2I_uppercase_hex func(c byte) bool { if c < 'A' || c > 'F'

(c byte)

//   return true
// }
func h2I(c byte) int {
	if c >= 48 && c <= 57 { // '0'..'9'
		return int(c - 48)
	}
	if c >= 65 && c <= 70 { // 'A'..'F'
		return int(c-65) + 10
	}
	if c >= 97 && c <= 102 { // 'a'..'f'
		return int(c-97) + 10
	}
	return badHex
}

// decodeSingleUnicodeEscape decodes a single \uXXXX escape sequence. The prefix \u is assumed to be present and
// is not checked.