return NULL;
 
        /* SGIs and PPIs */
-       if (intid <= VGIC_MAX_PRIVATE) {
-               intid = array_index_nospec(intid, VGIC_MAX_PRIVATE + 1);
+       if (intid < VGIC_NR_PRIVATE_IRQS) {
+               intid = array_index_nospec(intid, VGIC_NR_PRIVATE_IRQS);
                return &vcpu->arch.vgic_cpu.private_irqs[intid];
        }
 
 
 #define VGIC_NR_SGIS           16
 #define VGIC_NR_PPIS           16
 #define VGIC_NR_PRIVATE_IRQS   (VGIC_NR_SGIS + VGIC_NR_PPIS)
-#define VGIC_MAX_PRIVATE       (VGIC_NR_PRIVATE_IRQS - 1)
 #define VGIC_MAX_SPI           1019
 #define VGIC_MAX_RESERVED      1023
 #define VGIC_MIN_LPI           8192