Checked selection (RFC 0018)

WEAVEC_CHECKED attaches to a function declaration or definition and requests checking of its body. It supplies no trusted contract for an external body. weavec --checked selects input definitions; --checked-function=name can be repeated. The compiler equivalents are -fweavec-checked and -fweavec-checked-function=name. --checked-report=path (or the compiler’s -fweavec-checked-report=path) writes versioned JSON and computes contracts without selecting additional functions. See checked code.

The two checking diagnostics are errors by default and support the same -W controls as other IDs. Selected checking still fails when a diagnostic is demoted or suppressed: the proof status is independent of presentation.

RFC 0019 extends inferred memory contracts without adding annotations or diagnostic IDs. checking-incomplete reasons include read interval must be initialized, access interval must fit its object, callee initialized safety precondition must hold, and memcpy intervals must be disjoint. String calls also require a represented initialized terminator. Missing evidence remains distinct from a concrete checking-failed violation. Conditional memory and numeric output facts use summary format 23, sidecar format 24 and checked JSON version 2 (or compact version 3); rebuild older objects before link analysis.

RFC 0021 adds traversal contracts without new annotation spellings or IDs. Reasons include pointer difference or ordering needs shared-object evidence, pointer difference must fit target ptrdiff_t and element size, formed pointer must remain within its object or one past it, pointer arithmetic requires live non-null storage, and traversal requires an initialized terminated prefix. The last describes an inferred caller requirement. A failed caller may report callee terminated safety precondition must hold. The checked ledger retains separate bounds, initialization, validity and arithmetic obligations; an unresolved relationship does not assert a concrete invalid execution. Exhaustion remains explicit as traversal variable limit reached, traversal invariant candidate limit reached, or traversal relational limit reached. Diagnostic demotion does not make a limited contract complete.

Inductive chain diagnostics (RFC 0023)

Container inference adds no annotation or diagnostic identifier. checking-incomplete can report callee container chain precondition must hold or callee requires disjoint container footprints. The former requires actual live, initialized nodes with the requested read/write/release capability; the latter requires disjoint whole node and owned-payload footprints. Pointer inequality alone is insufficient. Cycles and unknown links do not satisfy a finite chain. Existing invalid-release, use-after-free and leak diagnostics remain active alongside these obligations. See linked containers.

Recursive ownership diagnostics (RFC 0027)

No new annotations or diagnostic ids are introduced. checking-incomplete can report callee recursive ownership precondition must hold for an unproved tree or forest, container operation loses part of the owned allocation footprint when cleanup or transfer is incomplete, and recursive cleanup does not establish complete input footprint consumption when a proposed recursive destructor cannot discharge its induction hypothesis. These messages describe failed proof obligations; ordinary leak, invalid-release, double-free and use-after-free checks remain active. A relation limit reports allocation footprint relation limit reached and cannot produce a complete contract. See recursive object ownership.

Runtime diagnostics (RFC 0024)

Runtime contracts reuse the two checking identifiers. Missing evidence can report runtime input interval must be initialized, runtime access interval must fit its object, runtime string requires an initialized terminator, or runtime operation requires a live C stream. Format reasons distinguish a missing argument, an incorrect promoted type, unsupported syntax, insufficient capacity and overlapping input/output. Fortified output also checks its object-size bound.

List diagnostics distinguish an inactive or consumed cursor (variadic traversal requires an active unconsumed argument list), an invalid start/copy/end operation, and an outstanding cleanup (locally started or copied argument list requires va_end). Raw byte writes and scope exit cannot discharge that obligation. A proven null dereference reports checking-failed with dereference requires a non-null pointer. No annotation or warning suppression grants runtime safety. Implicit output also requires a live standard stream, including through helpers that do not spell the stream argument. See C runtime contracts.

RFC 0025 adds the checking-incomplete reason read requires an initialized compatible union member. This requirement is independent of pointee lifetime, initialized bytes, bounds and ownership. A tag comparison cannot establish it. Unrepresented union storage reports union storage cannot be represented; a call whose input member path cannot be resolved reports union member requirement cannot be instantiated. No new annotation spelling or diagnostic identifier is introduced.

RFC 0026 adds buffer explanations under checking-incomplete: callee buffer allocation extent and initialized-prefix precondition must hold requires an established current buffer invariant; callee buffer backing storage requires allocation release permission distinguishes borrowed storage from an allocation the callee may release. owned buffer elements require complete release or transfer before container mutation preserves the independently owned pointee obligations. Initialized pointer bytes alone cannot discharge them. See growable buffers.

RFC 0028 carries these obligations across opaque public headers and private library state without new annotation spellings or diagnostic identifiers. Missing object evidence, incompatible layouts and unestablished private values retain incomplete checking; representation metadata alone grants no memory permission. Double cleanup and stale borrows retain their lifetime and ownership diagnostics across source units and compiler objects. See opaque objects and private library state for supported interfaces and required initialization.