Symbol: ptimer_intr
sys/kern/kern_time.c
100
static void ptimer_intr(void *);
sys/kern/kern_time.c
137
ptimer_intr, NULL);