tag	line	file	source code
RTC_SECONDS	56	kernel/time.c	time.sec = CMOS_READ(RTC_SECONDS);
RTC_SECONDS	62	kernel/time.c	} while (time.sec != CMOS_READ(RTC_SECONDS));
RTC_SECONDS	424	kernel/time.c	CMOS_WRITE(real_seconds,RTC_SECONDS);