vstd::raw_ptr

Function expose_provenance

Source 
pub exec fn expose_provenance<T: Sized>(m: *mut T) -> provenance : Tracked<IsExposed>
Expand description
ensures
provenance@@ == m@.provenance,

Perform a provenance expose operation.