Struct creusot_contracts::std::ptr::PtrDeepModel

pub struct PtrDeepModel {
    pub addr: Int,
    /* private fields */
}

We conservatively model raw pointers as having an address plus some hidden metadata.

This is to account for provenance (https://doc.rust-lang.org/std/ptr/index.html#using-strict-provenance) and wide pointers. See e.g. https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null: “unsized types have many possible null pointers, as only the raw data pointer is considered, not their length, vtable, etc. Therefore, two pointers that are null may still not compare equal to each other.”

Fields

addr: Int