I’m trying to get a better understand about the implementation details of seL4 for TK1-SOM.

Most of the code are very clear, but I’m little confused on the available physical memory in TK1-SOM.  I’m wondering why In the hardware.c file (/kernel/src/plat/tk1/machine/hardware.c), the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } instead of 0x80000000 - 0xffffffff?

Thank you very much!

-Dan