Struct MemoryContent 

pub(crate) struct MemoryContent<'z3, 'tcx> {
    pub(crate) byte_array: Option<Array<'z3>>,
    pub(crate) byte_written: FxHashSet<usize>,
    pub(crate) values: FxHashMap<(Ty<'tcx>, Vec<usize>), VmValue<'z3, 'tcx>>,
    pub(crate) facts: ContentFacts,
}

The per-allocation contents: the byte layer, the typed-value layer, and the content facts.

Fields

byte_array: Option<Array<'z3>>

Byte value function: byte[i] = select(array, i) for any (possibly symbolic) offset i. None when no byte has been written. Unwritten offsets read back the UNINIT sentinel, so init/nul are derived from select, not stored per byte.

byte_written: FxHashSet<usize>

The concrete byte offsets written to this allocation. Z3 arrays cannot enumerate their stored indices, so the byte-level checkers iterate this set directly instead of scanning the allocation’s (possibly symbolic or huge) size range. Only concrete writes are recorded: a symbolic byte_write (e.g. a symbolic ValidCStr length) still updates the byte array but not this set.

values: FxHashMap<(Ty<'tcx>, Vec<usize>), VmValue<'z3, 'tcx>>

The typed-value (Value) layer: (viewed_type, path) → value. path == [] is the allocation’s whole value (the rvalue bound to a local) and path == [i, ..] is field i, both viewed as viewed_type. The viewed_type distinguishes reinterprets of the same allocation under different ADTs (e.g. LeafNode vs InternalNode cast views), so field index 1 resolves to parent_idx under LeafNode and edges under InternalNode without colliding. This is the alloc-keyed counterpart to the byte-level Self::byte_array; the Local-keyed local_value/set_local/field_value/set_field_value resolve a local’s backing allocation and then read/write this layer.

facts: ContentFacts

Content facts (initialized/cstr_trusted/utf8_trusted); value-level facts live on each VmValue::facts.

Trait Implementations

impl<'z3, 'tcx> Default for MemoryContent<'z3, 'tcx>

fn default() -> Self

Returns the “default value” for a type.