Method read_u32

src/runtime.rs:261–269

#[ensures(effects!(old(trace), trace, effect!(ReadMem, addr, 4) if addr == start as usize))]

(&self, start: usize)

    #[ensures(trace_safe(trace, self))]
    // #[ensures(effects!(old(trace), trace, effect!(ReadMem, addr, 4) if addr == start as usize))]
    pub fn read_u32(&self, start: usize) -> u32 {
        let bytes: [u8; 4] = [
            self.mem[start],
            self.mem[start + 1],
            self.mem[start + 2],
            self.mem[start + 3],
        ];
        u32::from_le_bytes(bytes)
    }

    /// read u64 from wasm linear memory
    // Not thrilled about this implementation, but it works