Struct PointsToData

pub struct PointsToData<T> {
    pub ptr: *mut T,
    pub opt_value: MemContents<T>,
}

Data associated with a PointsTo permission. We keep track of both the pointer and the (potentially uninitialized) value it points to.

If opt_value is Init(T), this signifies that ptr points to initialized memory, and the value of opt_value is consistent with the bytes ptr points to, We also have all the ghost state associated with type T.

If opt_value is Uninit, then we have no knowledge about what’s in memory, and we assume ptr points to uninitialized memory. (To be pedantic, the bytes might be initialized in Rust’s abstract machine, but we don’t know, so we have to pretend they’re uninitialized.)

Fields

ptr: *mut T

opt_value: MemContents<T>