#include <stdio.h>
#include <stdint.h>

int main(void) {
	uint64_t ret = 0;
	ret = (((uint64_t)0x00000000000000FF) << 24);
	printf("#1 [%016llX]\n", ret);

	ret = 0;
	ret = (0x00000000000000FF << 24);
	printf("#2 [%016X]\n", ret);

	uint32_t ret2 = 0;
	ret2 = (((uint32_t)0x000000FF) << 8);
	printf("#3 [%08X]\n", ret2);

	ret2 = 0;
	ret2 = (0x000000FF << 8);
	printf("#4 [%08X]\n", ret2);
}
