#include <palacios/vmx_io.h>
#include <palacios/vmx_msr.h>
+
+#ifndef CONFIG_DEBUG_VMX
+#undef PrintDebug
+#define PrintDebug(fmt, args...)
+#endif
+
+
static addr_t host_vmcs_ptrs[CONFIG_MAX_CPUS] = { [0 ... CONFIG_MAX_CPUS - 1] = 0};
#define VMXASSIST_GDT 0x10000
addr_t vmxassist_gdt = 0;
- if (guest_pa_to_host_va(info, VMXASSIST_GDT, &vmxassist_gdt) == -1) {
+ if (v3_gpa_to_hva(info, VMXASSIST_GDT, &vmxassist_gdt) == -1) {
PrintError("Could not find VMXASSIST GDT destination\n");
return -1;
}
extern uint8_t v3_vmxassist_end[];
addr_t vmxassist_dst = 0;
- if (guest_pa_to_host_va(info, VMXASSIST_START, &vmxassist_dst) == -1) {
+ if (v3_gpa_to_hva(info, VMXASSIST_START, &vmxassist_dst) == -1) {
PrintError("Could not find VMXASSIST destination\n");
return -1;
}