vstd::raw_ptr

Function with_exposed_provenance

Source 
pub exec fn with_exposed_provenance<T: Sized>(
    addr: usize,
    verus_tmp_provenance: Tracked<IsExposed>,
) -> p : *mut T
Expand description
ensures
p
    == ptr_mut_from_data::<
        T,
    >(PtrData::<T> {
        addr: addr,
        provenance: provenance@,
        metadata: (),
    }),

Construct a pointer with the given provenance from a usize address. The provenance must have previously been exposed.