Skip to main content

pptr_usize_with_identity

ostd::specs::mm::frame::meta_owners

Function pptr_usize_with_identity 

Source 
pub proof fn pptr_usize_with_identity(p: PointsTo<usize>)
Expand description
ensures
pptr_usize_with(p, p.mem_contents()) == p,

Setting a PointsTo<usize> to its own contents is a no-op.