void kputhex(int out)
{       
        const char *hextable = "0123456789ABCDEF";
        char buffer[sizeof(int)*2 + 1] = {0};

        kputs("0x");
        for (int i = 0; i < sizeof(int)*2; i++) {
                buffer[sizeof(int)*2 - i] = hextable[out & 0x0F];
                kputc(hextable[out & 0x0F]);
                out = out >> 4;
        }
        
        kputs((char *)buffer);
}