Hi Ben,
As stated in the question, I'm not certain about how the integer part of the elements in the untyped_mmios array in devices.camkes are derived? "0xF1000000:24", "0xF2000000:25", "0xF4000000:26", "0xF8000000:24",
You are right that the numbers represent the size of the untyped mmios being created, 0xF1000000:24 -> [0xF1000000, 0xF1000000 + 0x1000000). In the example you gave, the four elements are defining a single ram region, but because the objects being created are seL4 untypeds that the vmm uses to construct the RAM device, there is an seL4 constraint that untyped objects can't be larger than their alignment. So camkes wouldn't be able to create an untyped object defined as: "0xF1000000:27" as this object would only have an alignment of 2^24 and seL4 would reject the retype invocation. Hope this answers your question.