#include <linux/kernel.h>
  #include <linux/list.h>
  #include <linux/smp.h>
 +#include <linux/cpu_pm.h>
  #include <linux/cpumask.h>
  #include <linux/io.h>
+ #include <linux/interrupt.h>
+ #include <linux/percpu.h>
+ #include <linux/slab.h>
  
  #include <asm/irq.h>
  #include <asm/mach/irq.h>
        if (gic_irqs > 1020)
                gic_irqs = 1020;
  
 +      gic->gic_irqs = gic_irqs;
 +
+       /*
+        * Nobody would be insane enough to use PPIs on a secondary
+        * GIC, right?
+        */
+       if (gic == &gic_data[0]) {
+               nrppis = (32 - irq_start) & 31;
+ 
+               /* The GIC only supports up to 16 PPIs. */
+               if (nrppis > 16)
+                       BUG();
+ 
+               ppi_base = gic->irq_offset + 32 - nrppis;
+       }
+ 
+       pr_info("Configuring GIC with %d sources (%d PPIs)\n",
+               gic_irqs, (gic == &gic_data[0]) ? nrppis : 0);
+ 
        /*
         * Set all global interrupts to be level triggered, active low.
         */