(ctx: &VmCtx, fd: HostFd)
| 274 | #[ensures(trace_safe(trace, ctx))] |
| 275 | #[ensures(effects!(old(trace), trace, effect!(FdAccess)))] |
| 276 | pub fn trace_sync(ctx: &VmCtx, fd: HostFd) -> RuntimeResult<usize> { |
| 277 | let os_fd: usize = fd.to_raw(); |
| 278 | let r = os_sync(os_fd); |
| 279 | RuntimeError::from_syscall_ret(r) |
| 280 | } |
| 281 | |
| 282 | #[with_ghost_var(trace: &mut Trace)] |
| 283 | #[requires(ctx_safe(ctx))] |