Method write_u64

src/runtime.rs:354–364

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

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

    #[ensures(trace_safe(trace, self))]
    // #[ensures(effects!(old(trace), trace, effect!(WriteMem, addr, 8) if addr == start as usize))]
    pub fn write_u64(&mut self, start: usize, v: u64) {
        let bytes: [u8; 8] = 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]);
        self.write_u8(start + 4, bytes[4]);
        self.write_u8(start + 5, bytes[5]);
        self.write_u8(start + 6, bytes[6]);
        self.write_u8(start + 7, bytes[7]);
    }

    #[with_ghost_var(trace: &mut Trace)]
    #[requires(ctx_safe(self))]