Method write_u16

src/runtime.rs:321–325

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

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

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

    /// write u32 to wasm linear memory
    // Not thrilled about this implementation, but it works