#include <stdio.h>

int main()
{
	printf("%f\n", 0x01234567);
	printf("%08x %08x\n");
	return 0;
}