Method write_u32

src/runtime.rs:337–343

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

(&mut self, start: usize, v: u32)

    #[ensures(trace_safe(trace, self))]
    // #[ensures(effects!(old(trace), trace, effect!(WriteMem, addr, 4) if addr == start as usize))]
    pub fn write_u32(&mut self, start: usize, v: u32) {
        let bytes: [u8; 4] = v.to_le_bytes();
        self.write_u8(start, bytes[0]);
        self.write_u8(start + 1, bytes[1]);
        self.write_u8(start + 2, bytes[2]);
        self.write_u8(start + 3, bytes[3]);
    }

    // TODO: replace with faster raw ptr memread/memwrite
    #[with_ghost_var(trace: &mut Trace)]