/* 7.2.2: unsigned big-endian 16-bit value. NOT USED IN KERNEL. */