pub proof fn pptr_usize_with_value(p: PointsTo<usize>, c: MemContents<usize>)Expand description
ensures
pptr_usize_with(p, c).mem_contents() == c,pptr_usize_with(p, c).pptr() == p.pptr(),