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

void u64function(uint64_t bar)
{
	printf("%llx\n", bar);
}

int main()
{
	uint32_t hi = 0xdeadbeef;
	uint32_t lo = 0xcafebabe;
	u64function((((uint64_t) hi) << 32) | lo);
	return 0;
}