VMX is working for a 32-bit Linux kernel. It should also work for a 64-bit kernel...

[palacios.git] / palacios / include / palacios / vmx_ctrl_regs.h

diff --git a/palacios/include/palacios/vmx_ctrl_regs.h b/palacios/include/palacios/vmx_ctrl_regs.h
index f35e878..88b24f4 100644 (file)
--- a/palacios/include/palacios/vmx_ctrl_regs.h
+++ b/palacios/include/palacios/vmx_ctrl_regs.h
@@ -2,4 +2,6 @@
 #include <palacios/vm_guest.h>
 #include <palacios/vmm_ctrl_regs.h>
 
-int v3_vmx_handle_cr0_write(struct guest_info * info, v3_reg_t new_val);
+int v3_vmx_handle_cr0_access(struct guest_info * info);
+int v3_vmx_handle_cr3_access(struct guest_info * info);
+