seL4 doesn't detect memory at runtime. The physical memory is specified in the DTS file, in this case, kernel/tools/dts/spike.dts
seL4 build system extracts the memory info from this file, generates platform headers, kernel/gen_headers/plat/machine/devices_gen.h
If you'd like to use smaller memory, simply modify the memory section in the DTS file.
________________________________________ From: Devel devel-bounces@sel4.systems on behalf of Porter, Jeremy porter.188@buckeyemail.osu.edu Sent: Saturday, 14 November 2020 6:57 AM To: devel@sel4.systems Subject: Re: [seL4] QEMU vs Spike on RISC-V Debugging
OK, this worked perfectly. Thank you!
Is there a reason we need so much memory? I've got the command you sent working with -m size=1025M, but I can't go lower. I've looked at machine.c code for the platform (spike) but that seems to adjust to the size provided by hardware.