| * Commonwealth Scientific and Industrial Research Organisation (CSIRO) |
| * This software may be distributed and modified according to the terms of |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. |
| * See "LICENSE_BSD2.txt" for details. |
| #include <vspace/arch/page.h> |
| #define SEL4_NUM_PAGE_SIZES ((int) ARRAY_SIZE(sel4_page_sizes)) |
| sel4_valid_size_bits(size_t size_bits) |
| for (int i = 0; i < SEL4_NUM_PAGE_SIZES && size_bits >= sel4_page_sizes[i]; i++) { |
| /* sanity check, sel4_page_sizes should be ordered */ |
| assert(sel4_page_sizes[i - 1] < sel4_page_sizes[i]); |
| if (size_bits == sel4_page_sizes[i]) { |
| sel4_page_size_bits_for_memory_region(size_t size_bytes) { |
| int frame_size_index = 0; |
| /* find the largest reasonable frame size */ |
| while (frame_size_index + 1 < SEL4_NUM_PAGE_SIZES) { |
| if (size_bytes >> sel4_page_sizes[frame_size_index + 1] == 0) { |
| return sel4_page_sizes[frame_size_index]; |