Method copy_buf_to_sandbox

src/runtime.rs:145–156

(
        &mut self,
        dst: SboxPtr,
        src: &Vec<u8>,
        n: u32,
    )

    #[ensures(trace_safe(trace, self))]
    #[ensures(self.memlen == old(self.memlen))]
    pub fn copy_buf_to_sandbox(
        &mut self,
        dst: SboxPtr,
        src: &Vec<u8>,
        n: u32,
    ) -> RuntimeResult<()> {
        if src.len() < n as usize || !self.fits_in_lin_mem(dst, n) {
            return Err(Efault);
        }
        self.memcpy_to_sandbox(dst, src, n);
        Ok(())
    }

    /// Copy arg buffer from from host to sandbox
    #[with_ghost_var(trace: &mut Trace)]