#[ensures(three_effects!(old(trace), trace, effect!(FdAccess), effect!(PathAccessAt, os_fd), effect!(WriteMem, addr, count)))]
(
ctx: &mut VmCtx,
dir_fd: HostFd,
pathname: HostPath,
ptr: SboxPtr,
cnt: usize,
)
| 416 | #[ensures(trace_safe(trace, ctx))] |
| 417 | // #[ensures(three_effects!(old(trace), trace, effect!(FdAccess), effect!(PathAccessAt, os_fd), effect!(WriteMem, addr, count)))] |
| 418 | pub fn trace_readlinkat( |
| 419 | ctx: &mut VmCtx, |
| 420 | dir_fd: HostFd, |
| 421 | pathname: HostPath, |
| 422 | ptr: SboxPtr, |
| 423 | cnt: usize, |
| 424 | ) -> RuntimeResult<usize> { |
| 425 | let slice = ctx.slice_mem_mut(ptr, cnt as u32); |
| 426 | let os_fd: usize = dir_fd.to_raw(); |
| 427 | // let os_path: Vec<u8> = pathname.into(); |
| 428 | let r = os_readlinkat(os_fd, pathname, slice, cnt); |
| 429 | RuntimeError::from_syscall_ret(r) |
| 430 | } |
| 431 | |
| 432 | #[with_ghost_var(trace: &mut Trace)] |
| 433 | #[requires(path_safe(&path, false))] |
no test coverage detected