#include <sys/types.h>
#include <sys/time.h>
#include <stdio.h>

static __inline sbintime_t
ustosbt2(int64_t _us)
{
	sbintime_t sb = 0;

#ifdef KASSERT
	KASSERT(_us >= 0, ("Negative values illegal for ustosbt: %jd", _us));
#endif
	if (_us >= 1000000) {
		sb = (_us / 1000000) * SBT_1S;
		_us = _us % 1000000;
	}
	/* 9223372036855 = ceil(2^63 / 1000000) */
	sb += ((_us * 9223372036855ull) + 0x7fffffff) >> 31;
	return (sb);
}


int main(int argc, char **argv) {
	int i;
	int64_t us[] = {0, 1, 999999, 1000000, 1000001, 1999999, 2000000,
		(1ll<<32) - 1, (1ll<<32)};

	for (i=0; i < 9; i++) {
		sbintime_t out = ustosbt(us[i]);
		sbintime_t out2 = ustosbt2(us[i]);

		printf("ustosbt(%10ld) = %10ld.%010ld "
		    "ustosbt2 = %10ld.%010ld\n",
		    us[i],
		    out >> 32, out & 0xFFFFFFFF,
		    out2 >> 32, out2 & 0xFFFFFFFF);
	}
	return (0);
}