#include <typedefs.h>

i64 cmos_get_time(void);
void cmos_set_time(i64 time);