-#if STAT_TIME
-
-#include <kern/macro_help.h>
-
-/* Advance a timer by the specified amount */
-#define TIMER_BUMP(timer, ticks) \
-MACRO_BEGIN \
- uint32_t old_low, low; \
- \
- old_low = (timer)->low_bits; \
- low = old_low + (ticks); \
- if (low < old_low) \
- timer_update((timer), (timer)->high_bits + 1, low); \
- else \
- (timer)->low_bits = low; \
-MACRO_END
-
-#define timer_switch(tstamp, new_timer)
-#define timer_event(tstamp, new_timer)
-
-#else /* STAT_TIME */
-
-/* Update the current timer and start a new one */
-extern void timer_switch(
- uint32_t tstamp,
- timer_t new_timer);
-
-#define TIMER_BUMP(timer, ticks)