Method create

src/fdmap.rs:108–112

#[requires(k < MAX_HOST_FDS)] #[ensures (self.lookup(k) == result)] #[ensures (forall(|i: usize| (i < MAX_SBOX_FDS && i != k) ==> self.lookup(i) == old(self.lookup(i))))] #[with_ghost_var(trace: &mut Trace)] #[external_call(Ok)] #[requires(trace_safe(ctx, trace))] #[ensures(trace_safe(ctx, trace))]

(&mut self, k: HostFd)

    // #[requires(trace_safe(ctx, trace))]
    // #[ensures(trace_safe(ctx, trace))]
    pub fn create(&mut self, k: HostFd) -> RuntimeResult<SboxFd> {
        let s_fd = self.pop_fd()?;
        self.m[s_fd as usize] = Ok(k);
        Ok(s_fd)
    }

    pub fn create_sock(&mut self, k: HostFd, proto: WasiProto) -> RuntimeResult<SboxFd> {
        let s_fd = self.pop_fd()?;