Skip to content
GUIDES

Check traversals and cursor helpers

RFC 0021 extends checked contracts to counted while and do loops, same-array cursors, guarded variable advances, and supported early exits. For example:

static char *fill(char *p, unsigned n) {
char *end = p + n;
while (p < end) *p++ = 1;
return p;
}
int main(void) {
char bytes[8];
char *end = fill(bytes, 8);
return end[-1];
}

The returned cursor is one past the initialized array. Reading end[0] still fails. Subtracting or ordering pointers requires live positions in the same array, compatible element types and a representable target result. Distinct array members of one structure do not become one array.

The checker preserves supported relationships such as output <= input through in-place compaction and complete pointer-to-pointer helpers. It checks every entry and back edge before retaining a loop fact. continue, skipped writes and early returns cannot establish an unwritten interval. Direct local goto follows the actual CFG and retains initialization and lifetime checks, including when it jumps into a loop or past a declaration.

Terminated scans require an initialized prefix through a known zero byte. That witness need not be the first zero. Reading a nonzero byte before the witness can justify advancing the cursor; lookahead has its own bounds. A potentially overlapping write must preserve the witness, establish a new zero, or lose the termination evidence. Separating pointer holders does not separate the arrays they reference.