openpic_read_irq
static __inline int openpic_read_irq(int);
return openpic_read_irq(curcpu()->ci_index);
openpic_read_irq(0);