Method try_write

security-monitor/src/core/page_allocator/allocator.rs:316–320

(op: O)

    #[rr::params("p")]
    #[rr::requires(#iris "once_initialized π \"PAGE_ALLOCATOR\" (Some ())")]
    #[rr::requires(#iris "□ ∀ x, {O::Pre} π p op x")]
    #[rr::exists("x")]
    #[rr::ensures(#iris "{O::Post} π p op x ret")]
    fn try_write<F, O>(op: O) -> Result<F, Error>
    where O: FnOnce(&mut RwLockWriteGuard<'static, PageAllocator>) -> Result<F, Error> {
        //op(&mut PAGE_ALLOCATOR.get().expect(Self::NOT_INITIALIZED).write())
        op(&mut PAGE_ALLOCATOR.get().unwrap().write())
    }