Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-04 14:31:12 +00:00
Code Issues Packages Projects Releases Wiki Activity

debug: always print TIMER_CLOCK_HZ as a uint64

Browse Source 
Signed-off-by: Axel Heider <axelheider@gmx.de>
This commit is contained in:
Axel Heider
2021-06-28 11:26:34 +02:00
committed by Kent McLeod
parent 32d81495fa
commit e65906dfa1
1 changed files with 8 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
src/drivers/timer/generic_timer.c
View File

@@ -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);
}
}