Skip to main content

extern_spec_core_ptr_addr_eq

creusot_std::std::ptr

Function extern_spec_core_ptr_addr_eq 

Source 
pub fn extern_spec_core_ptr_addr_eq<T, U>(p: *const T, q: *const U) -> bool
where
    T: ?Sized,
    U: ?Sized,
Expand description

extern spec for ::core::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())