diff --git a/include/plat/allwinnerA20/plat/machine/hardware.h b/include/plat/allwinnerA20/plat/machine/hardware.h
index 00a9b36110564d21170ce95f306f4851266295da..7e4b216e5bb89d03e35522ae126436991cb6caba 100755
--- a/include/plat/allwinnerA20/plat/machine/hardware.h
+++ b/include/plat/allwinnerA20/plat/machine/hardware.h
@@ -63,7 +63,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 /** MODIFIES: [*] */
diff --git a/include/plat/am335x/plat/machine/hardware.h b/include/plat/am335x/plat/machine/hardware.h
index 294cb55060b69d634bdee9d4a4ed3e99e7d4ea5c..29ea8a8944d40736b2cca07ec5f96a337b0ce95e 100644
--- a/include/plat/am335x/plat/machine/hardware.h
+++ b/include/plat/am335x/plat/machine/hardware.h
@@ -63,7 +63,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 void ackInterrupt(irq_t irq);
 bool_t isIRQPending(void);
diff --git a/include/plat/apq8064/plat/machine/hardware.h b/include/plat/apq8064/plat/machine/hardware.h
index c4cfab5a71eb62dcecc597ef06d0ede12a46c893..08f566915e515fc1554160741d137527aa28f068 100644
--- a/include/plat/apq8064/plat/machine/hardware.h
+++ b/include/plat/apq8064/plat/machine/hardware.h
@@ -66,7 +66,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 /** MODIFIES: [*] */
diff --git a/include/plat/exynos4/plat/machine/hardware.h b/include/plat/exynos4/plat/machine/hardware.h
index 34987ea760cd77d5d59b414a62b2e4fad2e06455..ec5f95790222f006ae33fe47543843dbac55bc52 100644
--- a/include/plat/exynos4/plat/machine/hardware.h
+++ b/include/plat/exynos4/plat/machine/hardware.h
@@ -75,7 +75,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 /** MODIFIES: [*] */
diff --git a/include/plat/exynos5/plat/machine/hardware.h b/include/plat/exynos5/plat/machine/hardware.h
index 14211ab1e07ee223bedf22a2ee9edd424ed0f77c..4b55c6d0b5f266d4e68a5c0ebe2b3b5ef6db27af 100644
--- a/include/plat/exynos5/plat/machine/hardware.h
+++ b/include/plat/exynos5/plat/machine/hardware.h
@@ -74,7 +74,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 /** MODIFIES: [*] */
diff --git a/include/plat/hikey/plat/machine/hardware.h b/include/plat/hikey/plat/machine/hardware.h
index 3adba10b26e0d6cd97240991fb0b307da3b8cfab..6f0a902b4166d0a8a5c98e7f8a638edd758f0dee 100755
--- a/include/plat/hikey/plat/machine/hardware.h
+++ b/include/plat/hikey/plat/machine/hardware.h
@@ -63,7 +63,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(unsigned int i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 /** MODIFIES: [*] */
diff --git a/include/plat/imx31/plat/machine/hardware.h b/include/plat/imx31/plat/machine/hardware.h
index f7d7148c80151743e1b467393df040396d9fc521..1f3eea8d4aba62bacd589efce742c4bae8946709 100644
--- a/include/plat/imx31/plat/machine/hardware.h
+++ b/include/plat/imx31/plat/machine/hardware.h
@@ -64,7 +64,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 void ackInterrupt(irq_t irq);
 bool_t isIRQPending(void);
diff --git a/include/plat/imx6/plat/machine/hardware.h b/include/plat/imx6/plat/machine/hardware.h
index 5b15d2a03136caf9b1589c27e16439dd9501d1bf..a23c5411c6a27e56bdd6c56753109408ecf7f345 100644
--- a/include/plat/imx6/plat/machine/hardware.h
+++ b/include/plat/imx6/plat/machine/hardware.h
@@ -76,7 +76,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 
diff --git a/include/plat/imx7/plat/machine/hardware.h b/include/plat/imx7/plat/machine/hardware.h
index c23635f7913094efcefe8e8aaa2b92af3bc6c07d..026193ba36997cf2bc3ef2023b7a1323c640a4e9 100644
--- a/include/plat/imx7/plat/machine/hardware.h
+++ b/include/plat/imx7/plat/machine/hardware.h
@@ -74,7 +74,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 static inline void
diff --git a/include/plat/omap3/plat/machine/hardware.h b/include/plat/omap3/plat/machine/hardware.h
index 294cb55060b69d634bdee9d4a4ed3e99e7d4ea5c..29ea8a8944d40736b2cca07ec5f96a337b0ce95e 100644
--- a/include/plat/omap3/plat/machine/hardware.h
+++ b/include/plat/omap3/plat/machine/hardware.h
@@ -63,7 +63,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 void ackInterrupt(irq_t irq);
 bool_t isIRQPending(void);
diff --git a/include/plat/tk1/plat/machine/hardware.h b/include/plat/tk1/plat/machine/hardware.h
index 98f3d6756b6605c67f4ba9f44cf9eb2e83a672c0..733cebb924b2b57c73544875c91a98d8ce3b1bdb 100644
--- a/include/plat/tk1/plat/machine/hardware.h
+++ b/include/plat/tk1/plat/machine/hardware.h
@@ -63,7 +63,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 /** MODIFIES: [*] */
diff --git a/include/plat/zynq7000/plat/machine/hardware.h b/include/plat/zynq7000/plat/machine/hardware.h
index 9a8ce2b06975e7c15e8a2af31a2447ea0233ddc3..07998c40c5d0b43296358a100c4891e7974c11bc 100644
--- a/include/plat/zynq7000/plat/machine/hardware.h
+++ b/include/plat/zynq7000/plat/machine/hardware.h
@@ -76,7 +76,6 @@ int get_num_dev_p_regs(void);
 p_region_t get_dev_p_reg(word_t i);
 void map_kernel_devices(void);
 
-bool_t CONST isReservedIRQ(irq_t irq);
 void handleReservedIRQ(irq_t irq);
 
 
diff --git a/src/plat/allwinnerA20/machine/hardware.c b/src/plat/allwinnerA20/machine/hardware.c
index c3e3ffe5a4b56815860fff54fb35c64353875723..1f9a1c5856aac75c19808b71f9233c6d200091c6 100755
--- a/src/plat/allwinnerA20/machine/hardware.c
+++ b/src/plat/allwinnerA20/machine/hardware.c
@@ -57,17 +57,6 @@ BOOT_CODE p_region_t get_dev_p_reg(word_t i)
     return dev_p_regs[i];
 }
 
-
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return  irq == KERNEL_TIMER_IRQ ||
-            irq == RESERVED_IRQ01   ||
-            irq == RESERVED_IRQ02   ||
-            irq == RESERVED_IRQ03;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/am335x/machine/hardware.c b/src/plat/am335x/machine/hardware.c
index e9457db3db35d8de5dd34a24b1e44cb4929c280c..0ed107b9761cdc83dae506f905da9b0bc3bf0d2f 100644
--- a/src/plat/am335x/machine/hardware.c
+++ b/src/plat/am335x/machine/hardware.c
@@ -219,13 +219,6 @@ maskInterrupt(bool_t disable, interrupt_t irq)
     }
 }
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t
-isReservedIRQ(interrupt_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void handleReservedIRQ(irq_t irq)
 {
diff --git a/src/plat/apq8064/machine/hardware.c b/src/plat/apq8064/machine/hardware.c
index ca384022986a30a0ec42eabb30b77eff2a483725..4ebae8e47c91363ed3fdd4e846cde6af00600f42 100644
--- a/src/plat/apq8064/machine/hardware.c
+++ b/src/plat/apq8064/machine/hardware.c
@@ -296,13 +296,6 @@ get_dev_p_reg(word_t i)
 }
 
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/exynos4/machine/hardware.c b/src/plat/exynos4/machine/hardware.c
index ced2a4647c789cc37bade1c9fd4fc3934abd7469..26ad4c223498103f681ad604f74f400a4ff15c4e 100644
--- a/src/plat/exynos4/machine/hardware.c
+++ b/src/plat/exynos4/machine/hardware.c
@@ -211,13 +211,6 @@ get_dev_p_reg(word_t i)
 }
 
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/exynos5/machine/hardware.c b/src/plat/exynos5/machine/hardware.c
index 246dc867d8ed266d8f608cc65b1390d714845638..cc99b24175d60b8c83e5b251cff165e37553c22c 100644
--- a/src/plat/exynos5/machine/hardware.c
+++ b/src/plat/exynos5/machine/hardware.c
@@ -270,14 +270,6 @@ get_dev_p_reg(word_t i)
     return dev_p_regs[i];
 }
 
-
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == INTERRUPT_WDT;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/hikey/machine/hardware.c b/src/plat/hikey/machine/hardware.c
index 3853870cc133a7a1910f485d0c0086ced10753e0..22bd1c9a078145f7446424bde81a568e488f5660 100644
--- a/src/plat/hikey/machine/hardware.c
+++ b/src/plat/hikey/machine/hardware.c
@@ -56,14 +56,6 @@ BOOT_CODE p_region_t get_dev_p_reg(unsigned int i)
     return dev_p_regs[i];
 }
 
-
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/imx31/machine/hardware.c b/src/plat/imx31/machine/hardware.c
index 651a44e2d671d4ee0ccd4d5af3bc48698da63d99..7163daf4b31321985cbf6a975031fe6b5b216c99 100644
--- a/src/plat/imx31/machine/hardware.c
+++ b/src/plat/imx31/machine/hardware.c
@@ -175,13 +175,6 @@ maskInterrupt(bool_t disable, interrupt_t irq)
     }
 }
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return false;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/imx6/machine/hardware.c b/src/plat/imx6/machine/hardware.c
index 3c0e1475f1d3893756377504eb83dc8c5fd7119e..66bdfb7c3ad67476a61dc8aa5d0d152fdea52168 100644
--- a/src/plat/imx6/machine/hardware.c
+++ b/src/plat/imx6/machine/hardware.c
@@ -194,14 +194,6 @@ get_dev_p_reg(word_t i)
     return dev_p_regs[i];
 }
 
-
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/imx7/machine/hardware.c b/src/plat/imx7/machine/hardware.c
index ccfc8c05e9e0e846db442c1c1762b1b25fc6a437..2590db869c2d7a5484b598c61665343fc7dba376 100644
--- a/src/plat/imx7/machine/hardware.c
+++ b/src/plat/imx7/machine/hardware.c
@@ -103,14 +103,6 @@ get_dev_p_reg(word_t i)
     return dev_p_regs[i];
 }
 
-
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/omap3/machine/hardware.c b/src/plat/omap3/machine/hardware.c
index 7e6d67615ba78179bdc1dab8c270725b39338772..5fbb2700b4f9ada618c68a9578d2796a965732f6 100644
--- a/src/plat/omap3/machine/hardware.c
+++ b/src/plat/omap3/machine/hardware.c
@@ -291,30 +291,6 @@ maskInterrupt(bool_t disable, interrupt_t irq)
     }
 }
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t
-isReservedIRQ(interrupt_t irq)
-{
-    return irq == RESERVED_IRQ01 ||
-           irq == RESERVED_IRQ02 ||
-           irq == RESERVED_IRQ03 ||
-           irq == RESERVED_IRQ04 ||
-           irq == RESERVED_IRQ05 ||
-           irq == RESERVED_IRQ06 ||
-           irq == RESERVED_IRQ07 ||
-           irq == RESERVED_IRQ08 ||
-           irq == RESERVED_IRQ09 ||
-           irq == RESERVED_IRQ10 ||
-           irq == RESERVED_IRQ11 ||
-           irq == RESERVED_IRQ12 ||
-           irq == RESERVED_IRQ13 ||
-           irq == RESERVED_IRQ14 ||
-           irq == RESERVED_IRQ15 ||
-           irq == RESERVED_IRQ16 ||
-           irq == RESERVED_IRQ17 ||
-           irq == RESERVED_IRQ18;
-}
-
 /* Handle a platform-reserved IRQ. */
 void handleReservedIRQ(irq_t irq)
 {
diff --git a/src/plat/tk1/machine/hardware.c b/src/plat/tk1/machine/hardware.c
index b879e05c87bbbdf91285d0d9a972a87913336678..d4dc98a7cbbedb74c8769a0dbe4825793cdb6c18 100644
--- a/src/plat/tk1/machine/hardware.c
+++ b/src/plat/tk1/machine/hardware.c
@@ -116,13 +116,6 @@ BOOT_CODE p_region_t get_dev_p_reg(word_t i)
 }
 
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)
diff --git a/src/plat/zynq7000/machine/hardware.c b/src/plat/zynq7000/machine/hardware.c
index 6f273303a71f5a28c5512784d3cad9229c7d2edf..a35a47f2852a5b46e5c04dcfe7f9eb9ebdb2fa44 100644
--- a/src/plat/zynq7000/machine/hardware.c
+++ b/src/plat/zynq7000/machine/hardware.c
@@ -114,13 +114,6 @@ get_dev_p_reg(word_t i)
 }
 
 
-/* Determine if the given IRQ should be reserved by the kernel. */
-bool_t CONST
-isReservedIRQ(irq_t irq)
-{
-    return irq == KERNEL_TIMER_IRQ;
-}
-
 /* Handle a platform-reserved IRQ. */
 void
 handleReservedIRQ(irq_t irq)