#[ensures(effects!(old(trace), trace, effect!(ReadMem, addr, 8) if addr == start as usize))]
(&self, start: usize)
| 280 | #[ensures(trace_safe(trace, self))] |
| 281 | // #[ensures(effects!(old(trace), trace, effect!(ReadMem, addr, 8) if addr == start as usize))] |
| 282 | pub fn read_u64(&self, start: usize) -> u64 { |
| 283 | let bytes: [u8; 8] = [ |
| 284 | self.mem[start], |
| 285 | self.mem[start + 1], |
| 286 | self.mem[start + 2], |
| 287 | self.mem[start + 3], |
| 288 | self.mem[start + 4], |
| 289 | self.mem[start + 5], |
| 290 | self.mem[start + 6], |
| 291 | self.mem[start + 7], |
| 292 | ]; |
| 293 | u64::from_le_bytes(bytes) |
| 294 | } |
| 295 | |
| 296 | /// read (u32,u32) from wasm linear memory |
| 297 | #[with_ghost_var(trace: &mut Trace)] |