 #ifndef CONFIG_SMP time_init_gtod(); #endif 
void __init time_init(void){	char *timename;#ifdef HPET_HACK_ENABLE_DANGEROUS        if (!vxtime.hpet_address) {		printk(KERN_WARNING "time.c: WARNING: Enabling HPET base "		       "manually!\n");                outl(0x800038a0, 0xcf8);                outl(0xff000001, 0xcfc);                outl(0x800038a0, 0xcf8);                vxtime.hpet_address = inl(0xcfc) & 0xfffffffe;		printk(KERN_WARNING "time.c: WARNING: Enabled HPET "		       "at %#lx.\n", vxtime.hpet_address);        }#endif	if (nohpet)		vxtime.hpet_address = 0;	xtime.tv_sec = get_cmos_time();	xtime.tv_nsec = 0;	set_normalized_timespec(&wall_to_monotonic,	                        -xtime.tv_sec, -xtime.tv_nsec);	if (!hpet_init()) {                vxtime_hz = (1000000000000000L + hpet_period / 2) /			hpet_period;		cpu_khz = hpet_calibrate_tsc();		timename = "HPET";	} else {		pit_init();		cpu_khz = pit_calibrate_tsc();		timename = "PIT";	}	printk(KERN_INFO "time.c: Using %ld.%06ld MHz %s timer.\n",	       vxtime_hz / 1000000, vxtime_hz % 1000000, timename);	printk(KERN_INFO "time.c: Detected %d.%03d MHz processor.\n",		cpu_khz / 1000, cpu_khz % 1000);	vxtime.mode = VXTIME_TSC;	vxtime.quot = (1000000L << 32) / vxtime_hz;	vxtime.tsc_quot = (1000L << 32) / cpu_khz;	vxtime.hz = vxtime_hz;	rdtscll_sync(&vxtime.last_tsc);	setup_irq(0, &irq0);	set_cyc2ns_scale(cpu_khz / 1000);}
4520	/local/tlutelli/issta_data/temp/c/2005_temp/2005/4520/a8ab26fe5bfeef43bdcde5182ca051ae0647607e/time.c/buggy/arch/x86_64/kernel/time.c