ps3_register_ipi_debug_brk   33 arch/powerpc/platforms/ps3/platform.h void __init ps3_register_ipi_debug_brk(unsigned int cpu, unsigned int virq);
ps3_register_ipi_debug_brk   87 arch/powerpc/platforms/ps3/smp.c 		ps3_register_ipi_debug_brk(cpu, virqs[PPC_MSG_NMI_IPI]);