diff --git a/repos/base-hw/src/core/spec/x86/platform_support.cc b/repos/base-hw/src/core/spec/x86/platform_support.cc
index 08e92dbbe5..494b3ea811 100644
--- a/repos/base-hw/src/core/spec/x86/platform_support.cc
+++ b/repos/base-hw/src/core/spec/x86/platform_support.cc
@@ -1,13 +1,14 @@
 /*
- * \brief   Platform implementations specific for base-hw and Raspberry Pi
+ * \brief   Platform implementations specific for x86
  * \author  Norman Feske
+ * \author  Reto Buerki
  * \date    2013-04-05
  *
  * XXX dimension allocators according to the available physical memory
  */
 
 /*
- * Copyright (C) 2013 Genode Labs GmbH
+ * Copyright (C) 2013-2015 Genode Labs GmbH
  *
  * This file is part of the Genode OS framework, which is distributed
  * under the terms of the GNU General Public License version 2.
@@ -15,6 +16,7 @@
 
 /* core includes */
 #include <platform.h>
+#include <board.h>
 #include <cpu.h>
 
 using namespace Genode;
@@ -42,6 +44,8 @@ Native_region * Platform::_core_only_mmio_regions(unsigned const i)
 {
 	static Native_region _regions[] =
 	{
+		{ Board::MMIO_LAPIC_BASE,  Board::MMIO_LAPIC_SIZE  },
+		{ Board::MMIO_IOAPIC_BASE, Board::MMIO_IOAPIC_SIZE },
 	};
 	return i < sizeof(_regions)/sizeof(_regions[0]) ? &_regions[i] : 0;
 }