Arrays and containers (RFC 0015)

Core/Array represents a selector as a constant or an immutable scalar plus an offset. Selected Index places live below array storage; the empty Index remains an unknown-element summary. Nested selections preserve each dimension. Moves, aliases, ownership, loans, nullness, callbacks and heap children use those ordinary places. AnalysisState adds sparse range-copy, fill and release facts, with must-facts weakened at joins. Limits are 32 selected cells and 32 range facts per storage object, independent of a program’s array length.

The Analysis implementation is split by operation: DataflowArrays.cpp resolves selectors and initializes cells, DataflowArrayMemory.cpp handles simultaneous copies and reallocations, DataflowArrayRanges.cpp retains copy snapshots, and the cleanup/fill files recognize and apply complete traversals. Scalar writes freeze index/count dependencies under bounded source-site identities. Unsupported generations and compositions retain explicit coverage information. Snapshots are analysis temporaries, not extra resource owners.

Summary paths encode selected constants and entry-parameter selectors. Final array-copy records carry storage paths, offsets, count, element size/view and guards; ordinary final cell postconditions take precedence. array-fill and array-release encode proved zero-based initialization and contiguous cleanup. Formats are deterministic and validated in Core, and global remapping visits every path, affine operand and guard. Returned ranges are captured before call effects and attached when the result obtains its destination. The normal function/program fixpoints compare these facts with the rest of the summary; compiler sidecars use the same format and inference.