Lines Matching refs:end
30 if (ndks_boot.reserved[i - 1].end == ndks_boot.reserved[i].start) { in merge_regions()
32 ndks_boot.reserved[i - 1].end = ndks_boot.reserved[i].end; in merge_regions()
49 assert(reg.start <= reg.end); in reserve_region()
50 if (reg.start == reg.end) { in reserve_region()
57 if (ndks_boot.reserved[i].start == reg.end) { in reserve_region()
62 if (ndks_boot.reserved[i].end == reg.start) { in reserve_region()
63 ndks_boot.reserved[i].end = reg.end; in reserve_region()
68 if (ndks_boot.reserved[i].start > reg.end) { in reserve_region()
73 reg.start, reg.end, (int)MAX_NUM_RESV_REG); in reserve_region()
89 reg.start, reg.end, (int)MAX_NUM_RESV_REG); in reserve_region()
101 assert(reg.start <= reg.end); in insert_region()
125 reg.start, reg.end, (unsigned int)MAX_NUM_FREEMEM_REG); in insert_region()
142 assert(rootserver_mem.start <= rootserver_mem.end); in alloc_rootserver_obj()
190 rootserver_mem.end = start + size; in create_rootserver_objects()
220 rootserver.paging.end = rootserver.paging.start + n * BIT(seL4_PageTableBits); in create_rootserver_objects()
231 assert(rootserver_mem.start == rootserver_mem.end); in create_rootserver_objects()
373 for (f = reg.start; f < reg.end; f += BIT(PAGE_BITS)) { in create_frames_of_region()
431 .end = ndks_boot.slot_pos_cur in init_sched_control()
607 unsigned int size_bits = seL4_WordBits - 1 - clzl(reg.end - reg.start); in create_untypeds_for_region()
649 (unsigned int)i, reg.start, reg.end); in create_untypeds()
654 start = ndks_boot.reserved[i].end; in create_untypeds()
665 reg.start, reg.end); in create_untypeds()
674 boot_mem_reuse_reg.start, boot_mem_reuse_reg.end); in create_untypeds()
685 (unsigned int)i, reg.start, reg.end); in create_untypeds()
692 .end = ndks_boot.slot_pos_cur in create_untypeds()
702 .end = BIT(CONFIG_ROOT_CNODE_SIZE_BITS) in bi_finalise()
730 printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end); in check_available_memory()
733 if (r->start > r->end) { in check_available_memory()
739 if (r->start == r->end) { in check_available_memory()
745 if ((i > 0) && (r->start < available[i - 1].end)) { in check_available_memory()
763 printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end); in check_reserved_memory()
766 if (r->start > r->end) { in check_reserved_memory()
772 if ((i > 0) && (r->start < reserved[i - 1].end)) { in check_reserved_memory()
808 avail_reg[i].end = ceiling_kernel_window(avail_reg[i].end); in init_freemem()
816 if (reserved[r].start == reserved[r].end) { in init_freemem()
819 } else if (avail_reg[a].start >= avail_reg[a].end) { in init_freemem()
822 } else if (reserved[r].end <= avail_reg[a].start) { in init_freemem()
826 } else if (reserved[r].start >= avail_reg[a].end) { in init_freemem()
835 avail_reg[a].start = MIN(avail_reg[a].end, reserved[r].end); in init_freemem()
839 assert(reserved[r].start < avail_reg[a].end); in init_freemem()
843 m.end = reserved[r].start; in init_freemem()
845 if (avail_reg[a].end > reserved[r].end) { in init_freemem()
846 avail_reg[a].start = reserved[r].end; in init_freemem()
857 if (reserved[r].start < reserved[r].end) { in init_freemem()
864 if (avail_reg[a].start < avail_reg[a].end) { in init_freemem()
899 pptr_t unaligned_start = ndks_boot.freemem[i].end - size; in init_freemem()
903 if (unaligned_start <= ndks_boot.freemem[i].end in init_freemem()
910 .end = ndks_boot.freemem[i].end in init_freemem()
913 ndks_boot.freemem[i].end = start; in init_freemem()