timer_set_base    553 kernel/timer.c 			timer_set_base(timer, NULL);
timer_set_base    557 kernel/timer.c 			timer_set_base(timer, base);
timer_set_base    585 kernel/timer.c 	timer_set_base(timer, base);
timer_set_base   1424 kernel/timer.c 		timer_set_base(timer, new_base);