#include <time.h>
#include "syscall.h"

clock_t clock(void)
{
	return syscall(VXSYSCLOCK, 0, 0, 0, 0, 0);
}