ACPI_FREQUENCY     41 dev/acpi/acpitimer.c 	ACPI_FREQUENCY,		/* frequency */
ACPI_FREQUENCY     95 dev/acpi/acpitimer.c 	printf(": %ld Hz, %d bits\n", ACPI_FREQUENCY,