Function extern_spec_core_ptr_metadata 

pub fn extern_spec_core_ptr_metadata<T: ?Sized>(
    ptr: *const T,
) -> <T as Pointee>::Metadata

extern spec for ::core::ptr::metadata<T>

This is not a real function: its only use is for documentation.

terminates

ghost

ensures

result == metadata_logic(ptr)