void __init setup_secondary_APIC_clock(void) 
void __cpuinit setup_secondary_APIC_clock(void) 
void __init setup_secondary_APIC_clock(void){	local_irq_disable(); /* FIXME: Do we need this? --RR */	setup_APIC_timer(calibration_result);	local_irq_enable();}
4520	/local/tlutelli/issta_data/temp/c/2005_temp/2005/4520/e6982c671c560da4a0bc5c908cbcbec12bd5991d/apic.c/clean/arch/x86_64/kernel/apic.c