SELFOUR-433: Shift as a 32-bit value
SELFOUR-433: Shift as a 32-bit value

Shifting as an unsigned long long does not work on some ARM compilers
as the kernel is not linked against libgcc

zhicheng/seL4,cmr/seL4,zhicheng/seL4,zhicheng/seL4,cmr/seL4,cmr/seL4