From e65906dfa115bfbd9e7e36e37dde11781da27cc9 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Mon, 28 Jun 2021 11:26:34 +0200 Subject: [PATCH] debug: always print TIMER_CLOCK_HZ as a uint64 Signed-off-by: Axel Heider --- src/drivers/timer/generic_timer.c | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/drivers/timer/generic_timer.c b/src/drivers/timer/generic_timer.c index 027413712..3dc000b62 100644 --- a/src/drivers/timer/generic_timer.c +++ b/src/drivers/timer/generic_timer.c @@ -15,9 +15,14 @@ BOOT_CODE void initGenericTimer(void) /* The CNTFRQ register is a 32-bit register, its value can safely be * compared with TIMER_CLOCK_HZ. */ - if (gpt_cntfrq != 0 && gpt_cntfrq != TIMER_CLOCK_HZ) { - printf("Warning: gpt_cntfrq %"SEL4_PRIu_word", expected %u\n", - gpt_cntfrq, (uint32_t)TIMER_CLOCK_HZ); + if ((gpt_cntfrq != 0) && (gpt_cntfrq != TIMER_CLOCK_HZ)) { + /* TIMER_CLOCK_HZ is supposed to be a 64-bit value, but that is not + * really enforced, it could be any integer type. Variable args + * require the type to be very well defined to work properly, so + * casting explicitly to unit64_t here is the best option. + */ + printf("Warning: gpt_cntfrq %"SEL4_PRIu_word", expected %"PRIu64"\n", + gpt_cntfrq, (uint64_t)TIMER_CLOCK_HZ); } }