Function extern_spec_std_ptr_metadata 

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

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

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

terminates

ghost

ensures

result == metadata_logic(ptr)