Function trace_socket

src/os/mod.rs:652–655

(ctx: &VmCtx, domain: i32, ty: i32, protocol: i32)

#[ensures(trace_safe(trace, ctx))]
#[ensures(effects!(old(trace), trace, effect!(SockCreation, d, t) if d == domain as usize && t == ty as usize ))]
pub fn trace_socket(ctx: &VmCtx, domain: i32, ty: i32, protocol: i32) -> RuntimeResult<usize> {
    let r = os_socket(domain, ty, protocol);
    RuntimeError::from_syscall_ret(r)
}

#[with_ghost_var(trace: &mut Trace)]
#[requires(addr_in_netlist(&ctx.netlist, addr.sin_addr.s_addr, addr.sin_port as u32))]