#define VMEXIT_DR15_READ 0x0000002f
#define VMEXIT_DR_WRITE_MASK 0xffffffc0
-#define VMEXIT_DR0_WRITE 0x0000003f
+#define VMEXIT_DR0_WRITE 0x00000030 // ? this was previously 3f
#define VMEXIT_DR1_WRITE 0x00000031
#define VMEXIT_DR2_WRITE 0x00000032
#define VMEXIT_DR3_WRITE 0x00000033
--- /dev/null
+#ifndef __SVM_WBINVD_H
+#define __SVM_WBINVD_H
+
+#ifdef __V3VEE__
+
+#include <palacios/vm_guest.h>
+#include <palacios/vmcb.h>
+#include <palacios/vmm.h>
+
+
+int handle_svm_wbinvd(struct guest_info * info);
+
+
+#endif // ! __V3VEE__
+
+#endif