C integers and dynamic bounds

RFC 0017 adds no annotation spellings. WEAVEC_SIZED_BY(n) still counts elements (void * counts bytes), and WEAVEC_ASSUME still supplies a trusted invariant. Both use the expressions’ actual C types. Neither contract changes an allocation’s size or establishes whole-program verification.

Integer interpretation now affects temporal checks as well as bounds. On an eight-bit-char target, this narrowing cannot hide the use-after-free:

#include <stdlib.h>

void example(unsigned n) {
  if (n != 256) return;
  unsigned char k = n;       // k is zero
  char *p = malloc(1);
  if (!p) return;
  free(p);
  if (k == 0) *p = 1;       // use-after-free
}

For supported types through 64 bits, promotions and storage conversions apply to assignments, compound assignments, comparisons, switches, selected indices and count adjustments. Unsigned arithmetic wraps modulo its width. Signed arithmetic retains its validity rules, with wrapping arithmetic honored where the compilation mode defines it. The checker reports definitely invalid operations it visits; it is not a general integer lint for all expressions.

Allocation extents use the value actually passed: malloc((unsigned char)n) on that target receives zero when n == 256. A repeated symbolic byte product can expose p[rows * cols] as one past malloc(rows * cols), even when the unsigned product wraps. The byte interval of an access is then calculated mathematically, without wrapping its end back into the allocation. Supported __builtin_add_overflow, __builtin_sub_overflow and __builtin_mul_overflow calls retain their output and success/failure facts; a matching nonzero-divisor and SIZE_MAX / count guard can establish that a product fits. calloc and reallocarray use checked products: overflow cannot create a small successful allocation, and failed reallocarray retains its input object.

Numeric returns and out-parameters retain representable expressions and guards through helpers, translation units and compiler sidecars. Access requirements retain lower bounds and numeric conditions. A supported zero-based unit-stride loop with i < n && i < cap can require min(n, cap) elements; equivalent explicit minimum expressions also compose. Early-exit and other unsupported loops do not produce inferred must-requirements: a bound that the loop might reach cannot be treated as storage every caller must provide. Reassigning a size operand does not resize an earlier allocation or output snapshot.

VLA dimensions are captured at declaration time, including supported nested dimensions and subsequent sizeof of that array. A later write to the bound variable does not change the existing array. A definitely nonpositive dimension is invalid-integer-operation; an unrepresentable byte extent remains incomplete. Flexible-array member bounds come from the backing allocation minus the target’s field offset, with the member’s element size. A sibling count cannot invent tail storage. Tail pointers preserve the enclosing allocation’s lifetime and release identity, while fixed-array subobjects retain their own bounds. Inferred sized fields preserve the C type of count multiplication, including its possible wrap.

The dump reports spatial: proven=<n> violation=<n> unresolved=<n> per function, with unresolved reason counts. proven covers the full represented access, including its lower bound; violation follows the existing definite or supported reachable-boundary policy; unresolved means the check was not decided. Reasons include unknown extent, unknown pointer offset, unknown index bounds, unrepresentable byte arithmetic, unsupported numeric expression and caller requirement. A requirement still needs its callers checked. Counts are independent of diagnostic suppression: WEAVEC_UNSAFE retains numeric effects and spatial outcomes while suppressing reports, and changing warning severity does not turn an unresolved access into a proof.

Ranges retain at most two intervals; symbolic expressions have at most 64 nodes and depth 12, and guards at most eight conjuncts including numeric predicates. Numeric outputs retain at most eight alternatives. Unsupported projection or exhausted bounds can report analysis-incomplete; an arbitrary unknown index alone remains unresolved without a new bounds error. General nonlinear inequalities, arbitrary induction/strides, integers wider than 64 bits, unsupported union/type-punning and pointer-provenance operations, unrestricted aliases, byte-encoded pointers, GC invariants and concurrency remain outside the supported model.

RFC 0017 introduced summary and sidecar format 13. Current summary format 23 and sidecar format 24 require rebuilding older objects. The RFC 0017 validation report records passing regression and sanitizer suites, corpus coverage, performance costs and remaining false positives. No runtime instrumentation, --verify flag or verification certificate is introduced.