Symbol: vmx_change_cpu
sys/dev/nvmm/x86/nvmm_x86_vmx.c
3800
xc = xc_broadcast(0, vmx_change_cpu, (void *)false, NULL);
sys/dev/nvmm/x86/nvmm_x86_vmx.c
3809
xc = xc_broadcast(0, vmx_change_cpu, (void *)true, NULL);