diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index dacacdb29..60e8f7518 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -74,7 +74,7 @@ void debug_print_bootinfo(seL4_BootInfo *info) printf("extra boot info blobs:\n"); seL4_Word offs = 0; while (offs < info->extraLen) { - seL4_BootInfoHeader *h = (seL4_BootInfoHeader *)((seL4_Word)info + 4096 + offs); + seL4_BootInfoHeader *h = (seL4_BootInfoHeader *)((seL4_Word)info + SEL4_BI_FRAME_SIZE + offs); printf(" type: %"SEL4_PRIu_word", offset: %"SEL4_PRIu_word", len: %"SEL4_PRIu_word"\n", h->id, offs, h->len); offs += h->len;