Understand contracts

static void touch(char *p, unsigned n) {
  for (unsigned i = 0; i < n; ++i) {
    if (p[i] == 42) break;
    p[i] = 1;
  }
}

This helper may access any byte in [0,n), even though it can exit early. Its sufficient contract requires live memory with that accessible, initialized and writable interval. A caller providing four initialized bytes can satisfy touch(p,4); it cannot establish touch(p,8) from those facts. The latter is an unresolved precondition, without claiming that execution necessarily reaches byte eight.

Supported private globals retain their identities and conditions in exported requirements (RFC 0028). A caller can establish such a condition through a verified initializer or setter. Unsupported private storage can still require stronger entry assumptions or prevent complete export; a missing premise never becomes an assumed fact or disappears from an output guarantee.

Write permission is a separate requirement: string literals and const objects remain read-only even through a cast. Mutable local objects and modeled allocations provide positive writability evidence; helper callers must establish exported writable intervals.

Ownership alone does not initialize memory. malloc storage needs writes before reads; calloc supplies zeroed bytes. Writing one cell does not establish another cell. At branch joins, initialization is retained only where every incoming path establishes it. Supported complete copies establish the copied range. Complete helper contracts can export initialization postconditions.

A verified cleanup wrapper can export allocation-consumed for a pointer parameter. This guarantees cleanup of that entry allocation, including a null entry that has nothing to release. It does not cover child allocations or buffer payloads; complete container cleanup needs container-consumed and its ownership requirements. A conditional or omitted free cannot establish an unconditional cleanup output. Current forwarding supports unconditional outputs for direct pointer parameters and the free allocation family.

For example, a complete fill establishes the bytes that a later read needs:

static void fill(char *bytes, unsigned size) {
  for (unsigned i = 0; i < size; ++i) bytes[i] = 1;
}
int main(void) {
  char bytes[8];
  fill(bytes, 8);
  return bytes[7];
}

Skipping a store or exiting the loop early cannot establish that full interval. The same output facts can cross nested buffer fields, allocation-returning constructors and successful output parameters. A status test selects only facts guaranteed for that outcome; overwriting an output or its length retires the earlier facts. A saved alias of a released object remains invalid after a helper installs a replacement.

memcpy checks disjoint intervals, including slices of the same object. memmove uses the source’s initialization before the move. Positive-size realloc preserves initialized bytes within the old and new extents on success; its grown tail needs writes. Failure retains the incoming storage. String models check accessible initialized data through a terminator. A known zero byte can witness termination without inventing an exact length.