Method initialize

security-monitor/src/core/page_allocator/allocator.rs:88–97

(memory_start: ConfidentialMemoryAddress, memory_end: *const usize)

    #[rr::ensures(#iris "once_initialized π \"PAGE_ALLOCATOR\" (Some ())")]
    #[rr::returns("Ok(())")]
    pub unsafe fn initialize(memory_start: ConfidentialMemoryAddress, memory_end: *const usize) -> Result<(), Error> {
        ensure_not!(PAGE_ALLOCATOR.is_completed(), Error::Reinitialization())?;
        let mut page_allocator = Self::empty();
        unsafe { page_allocator.add_memory_region(memory_start, memory_end)? };
        PAGE_ALLOCATOR.call_once(
            #[rr::verify]
            || RwLock::new(page_allocator),
        );
        Ok(())
    }

    /// Specification:
    /// Postcondition: an initialized memory allocator is returned