diff --git a/repos/base-hw/src/core/kernel/kernel.cc b/repos/base-hw/src/core/kernel/kernel.cc
index a44d004f2..8808489b1 100644
--- a/repos/base-hw/src/core/kernel/kernel.cc
+++ b/repos/base-hw/src/core/kernel/kernel.cc
@@ -303,8 +303,8 @@ extern "C" void init_kernel_multiprocessor()
 		t.init(processor, core_pd(), &utcb, 1);
 
 		/* initialize interrupt objects */
-		static Genode::uint8_t _irqs[Pic::MAX_INTERRUPT_ID * sizeof(Irq)];
-		for (unsigned i = 0; i < Pic::MAX_INTERRUPT_ID; i++) {
+		static Genode::uint8_t _irqs[(Pic::MAX_INTERRUPT_ID+1) * sizeof(Irq)];
+		for (unsigned i = 0; i <= Pic::MAX_INTERRUPT_ID; i++) {
 			if (private_interrupt(i)) { continue; }
 			new (&_irqs[i * sizeof(Irq)]) Irq(i);
 		}
diff --git a/repos/base-hw/src/core/platform.cc b/repos/base-hw/src/core/platform.cc
index 06ab5dd07..9b9ecb5f2 100644
--- a/repos/base-hw/src/core/platform.cc
+++ b/repos/base-hw/src/core/platform.cc
@@ -132,7 +132,7 @@ Platform::Platform()
 	           _core_only_ram_regions, get_page_size_log2());
 
 	/* make interrupts available to the interrupt allocator */
-	for (unsigned i = 0; i < Kernel::Pic::MAX_INTERRUPT_ID; i++)
+	for (unsigned i = 0; i <= Kernel::Pic::MAX_INTERRUPT_ID; i++)
 		_irq_alloc.add_range(i, 1);
 
 	/*