pub fn extern_spec_std_ptr_addr_eq<T, U>(p: *const T, q: *const U) -> boolExpand description
extern spec for ::std::ptr::addr_eq<T, U>
This is not a real function: its only use is for documentation.
terminates
ghost
ensures
result == (p.addr_logic() == q.addr_logic())