Symbol: vmx_vmlaunch
sys/dev/nvmm/x86/nvmm_x86_vmx.c
2453
ret = vmx_vmlaunch(cpudata->gprs);
sys/dev/nvmm/x86/nvmm_x86_vmx.c
61
int vmx_vmlaunch(uint64_t *gprs);