Skip to main content

_verus_external_fn_specification_8__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq

vstd::raw_ptr

Function _verus_external_fn_specification_8__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq 

Source 
pub unsafe exec fn _verus_external_fn_specification_8__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq<T: PointeeSized>(
    x: &*mut T,
    y: &*mut T,
) -> res : bool
Expand description
ensures
res <==> (x@.addr == y@.addr) && (x@.metadata == y@.metadata),

Specification for <*mut T as PartialEq<*mut T>>::eq Compares the address and metadata of two pointers.

Note that this does NOT compare provenance, which does not exist in the runtime pointer representation (i.e., it only exists in the Rust abstract machine).