Checked C interfaces (RFC 0022)

Core/ObjectType validates portable byte size, alignment and canonical view identity; it has no Clang dependency. DataflowObjectTypes.cpp builds target views and discharges erased-pointer recovery at evaluated CFG points. Object views live on checked storage identities. Conflicting or missing predecessor views become unknown, distinct from untyped fresh allocated storage.

CheckedRequirement::ifNonNull is an output-value condition on initialized, zeroed or copied bytes. Call-entry conditions are captured before stores; the output pointer is resolved after them. Return merging permits a final-null edge to satisfy this conditional guarantee, retaining only null paths proved on every preceding edge. Unknown non-null bytes never acquire initialization.

Callback contexts remap global paths and reject any lost binding. Sidecars serialize the names of globals in callback contexts as in memory contexts. A global-name prelude retains the producer’s name-table order, including unused identities, so decoding cannot reorder callback inputs or context keys. The table contributes no storage or callback facts. GlobalTable provides portable identities for supported private static storage, including local statics, nested records and fixed arrays (RFC 0028). Foreign units use implicit storage adapters outside source declaration lookup; the defining unit resolves them to the original variable. Checked invocation uses established reaching targets and preserves singleton library provenance for allocation, memory and string rules. DataflowCheckedCallbacks.cpp checks each resolved alternative against a separate call-entry state and intersects its guaranteed outputs over returning targets. Unknown alternatives remain coverage boundaries; no contract is inferred from a callback’s prototype alone.