Index: kernel/arch/ia32/include/drivers/i8259.h
===================================================================
--- kernel/arch/ia32/include/drivers/i8259.h	(revision df4ed852a2d1b242f9bdce0a873009a2cb77cec7)
+++ kernel/arch/ia32/include/drivers/i8259.h	(revision dc22844fb0d5ea9ccfad3f1097a7bf38da0c0ef9)
@@ -39,8 +39,8 @@
 #include <arch/interrupt.h>
 
-#define PIC_PIC0PORT1	0x20
-#define PIC_PIC0PORT2	0x21
-#define PIC_PIC1PORT1	0xa0
-#define PIC_PIC1PORT2	0xa1
+#define PIC_PIC0PORT1	((ioport8_t *) 0x20)
+#define PIC_PIC0PORT2	((ioport8_t *) 0x21)
+#define PIC_PIC1PORT1	((ioport8_t *) 0xa0)
+#define PIC_PIC1PORT2	((ioport8_t *) 0xa1)
 
 #define PIC_NEEDICW4	(1<<0)