/* @value: value to be printed @prec: minimum number of digits to display @buf: pointer to buffer address on return position of terminating zero word  */
static void uint2dec(u32 value, int prec, u16 **buf)
/* @value: value to be printed @prec: minimum number of digits to display @buf: pointer to buffer address on return position of terminating zero word  */
static void uint2dec(u32 value, int prec, u16 **buf)
{
	u16 *pos = *buf;
	int i;
	u16 c;
	u64 f;
	f = 0x225C17D0;
	f += (0x9B5A52DULL * value) >> 28;
	f += 0x44B82FA0ULL * value;
	for (i = 0; i < 10; ++i) {
		c = f >> 60;
		if (c || pos != *buf || 10 - i <= prec)
			*pos++ = c + '0';
		f &= 0xfffffffffffffff;
		f *= 0xaULL;
	}
	if (pos == *buf)
		*pos++ = '0';
	*pos = 0;
	*buf = pos;
}