Symbol: vtimer_init
sys/arm64/vmm/io/vtimer.h
69
int vtimer_init(void);
sys/arm64/vmm/vmm_arm64.c
444
vtimer_init();