Note that this required adding missing ()'s around the outermost level
of MSK_READ_MIB*. Otherwise, the void cast was only applied to the
first register read. This also meant that MSK_READ_MIB64 was pretty
broken as the uint64_t cast only applied to the first 16-bit register
read in each MSK_READ_MIB32 invocation and the 32-bit shift was only
applied to the second register read of the pair.
Reported by: GCC -Wunused-value