Method copy_environ_buffer_to_sandbox

src/runtime.rs:184–192

(&mut self, dst: SboxPtr, n: u32)

    #[ensures(ctx_safe(self))]
    #[ensures(trace_safe(trace, self))]
    pub fn copy_environ_buffer_to_sandbox(&mut self, dst: SboxPtr, n: u32) -> RuntimeResult<()> {
        if !self.fits_in_lin_mem(dst, n) {
            return Err(Efault);
        }
        // let env_buffer = self.env_buffer.clone();
        let env_buffer = clone_vec_u8(&self.env_buffer);
        self.memcpy_to_sandbox(dst, &env_buffer, n);
        Ok(())
    }

    #[with_ghost_var(trace: &mut Trace)]
    #[external_calls(resolve_path)]