/* 7.3.2: unsigned big-endian 32-bit value. NOT USED IN KERNEL. */