Method pop_fd

src/fdmap.rs:87–98

#[with_ghost_var(trace: &mut Trace)] #[external_call(Ok)] #[external_call(Err)] #[external_method(pop)]

(&mut self)

    // #[external_call(Err)]
    // #[external_method(pop)]
    fn pop_fd(&mut self) -> RuntimeResult<SboxFd> {
        match self.reserve.pop() {
            Some(fd) => Ok(fd),
            None => {
                if self.counter < MAX_SBOX_FDS {
                    self.counter += 1;
                    return Ok(self.counter - 1);
                }
                Err(Emfile)
            }
        }
    }

    // #[requires(k < MAX_HOST_FDS)]
    // #[ensures (self.lookup(k) == result)]