#include <arch/x86/apic.h>
#include <arch/x86/global.h>
#include <arch/x86/perfmon.h>
-#include <vmkit.h>
-#include <barrelfish_kpi/sys_debug.h>
-#include <barrelfish_kpi/lmp.h>
-#include <barrelfish_kpi/dispatcher_shared_target.h>
#include <arch/x86/debugregs.h>
-#include <trace/trace.h>
#include <arch/x86/syscall.h>
#include <arch/x86/timing.h>
-#include <fpu.h>
#include <arch/x86/ipi_notify.h>
+#include <barrelfish_kpi/sys_debug.h>
+#include <barrelfish_kpi/lmp.h>
+#include <barrelfish_kpi/dispatcher_shared_target.h>
+#include <trace/trace.h>
+#ifndef __k1om__
+#include <vmkit.h>
- #include <amd_vmcb_dev.h>
+ #include <dev/amd_vmcb_dev.h>
+#endif
#define MIN(a,b) ((a) < (b) ? (a) : (b))