Coming from the embedded world, where even uclibc is not always available, and code like
uint64_t myval = 0xdeadfacedeadbeef;
printf("%llx", myval);
is printing you crap or not working at all -- i always use a tiny helper, that allows me to dump properly uint64_t hex:
#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>
char* ullx(uint64_t val)
{
static char buf[34] = { [0 ... 33] = 0 };
char* out = &buf[33];
uint64_t hval = val;
unsigned int hbase = 16;
do {
*out = "0123456789abcdef"[hval % hbase];
--out;
hval /= hbase;
} while(hval);
*out-- = 'x', *out = '0';
return out;
}