Function vstd::raw_ptr::with_exposed_provenance

source ·

pub exec fn with_exposed_provenance<T: Sized>(
    addr: usize,
    verus_tmp_provenance: Tracked<IsExposed>
) -> *mut T

Expand description

ensures

p
    == ptr_mut_from_data::<
        T,
    >(PtrData {
        addr: addr,
        provenance: provenance@,
        metadata: Metadata::Thin,
    }),

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