Miscellany

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

int main() {
        uint64_t v = 12345467227327892LL;
        printf("%02lx%02lx%02lx%02lx\n",
                        v << 48,
                        v << 32 & 0xFFFF,
                        v << 16 & 0xFFFF,
                        v & 0xFFFF
        );
}