What the checker understands

• Ownership sources: malloc, calloc, realloc, strdup, strndup, aligned_alloc, fopen, opendir, getaddrinfo, asprintf, getline, mmap, pthread_create, … (the shipped libc/POSIX table, about 490 functions from <stdlib.h>, <stdio.h>, <string.h>, <unistd.h>, <fcntl.h>, <dirent.h>, <sys/mman.h>, <netdb.h>, <pthread.h>, <time.h>, <pwd.h>, <grp.h>, <regex.h>, <dlfcn.h>, <wchar.h> and friends), any function whose return type carries WEAVEC_OWNED, and any function defined in the program whose body returns a fresh allocation.
• Releases and moves: free, fclose, closedir, freeaddrinfo, munmap, regfree, dlclose, …, passing a pointer to a WEAVEC_OWNED parameter, and passing it to a function defined in the program whose body frees or moves that parameter (through any depth of wrappers and through recursion). realloc(p, n) moves p; on the path where the result is tested null (if (!q), q == NULL, …), p is valid again.
• Resource lifecycle (RFC 0007): every ownership source above puts a resource on the function’s books, with the release family of its allocator (free, fclose, closedir, freeaddrinfo, munmap, pclose, regfree, dlclose, …; a WEAVEC_OWNED parameter’s family is unknown). It leaves the books when it is released by a function of the same family, moved into an owning parameter, returned, stored into caller-visible memory (*out, b->data, a global), copied into a struct that is returned or stored, handed to a callee the checker cannot follow, or cast to an integer. A resource still on the books when its last holder dies is a leak; a release by another family is a mismatched-release. Copies share one record (q = p; ... use(q); reports q once), a callee summarised from its body that keeps nothing is trusted not to retain the argument, and the null edge of a test of the holder (if (!p) return -1;) owns nothing. A constructor that reports failure through its result (int make(char **out) { *out = malloc(n); return *out != NULL; }) is summarised with the classes on which *out is null, so if (!make(&s)) return; is clean.
• Outcome-conditional consumption (RFC 0006): a callee that frees or moves its argument only on the paths that return some class of value (NULL vs non-null, 0 vs positive vs negative) is summarised per class, and a test of its result selects the class: after int rc = try_take(p); the pointer p is gone where rc == 0 and still yours where rc != 0, if try_take frees only when it returns 0. Recognised tests: x, !x, x == NULL, x != NULL, x == 0, x != 0 and comparisons with an integer constant (x < 0, x == -1, x >= 0, …), on the call itself, on the variable its result was stored in, or on an assignment inside the condition (if ((rc = f(p)) < 0)). Wrappers (char *q = realloc(p, n); if (!q) return NULL; return q;) inherit the conditional behaviour. Untested, a conditional free is a may-free and the next use is reported.
• Calls through function pointers: the callee’s signature is taken from the annotations on the function-pointer type (typedef, field or parameter) when it has any; otherwise from the join of the summaries of every function of that type whose address is taken anywhere in the program (ops.drop = node_free;, qsort(a, n, sz, cmp)), so a call through ops->drop frees what node_free frees. Pointers with neither are reported once per type as annotation-required.
• The program: with weavec file.c -- the program is that one file; with weavec --whole-program or weavec-cc it is every file analysed or linked together, and a callee defined in another file is checked from its body there (a definition wins over the libc table, so a program that defines its own strdup is checked against its own). A whole-struct copy b = a copies the facts of every pointer field, so b = a; free(a.data); b.data[0] is a use after free.
• Effects through parameters: a callee that frees b->data, writes *out, or stores a fresh allocation into *out or a global has that effect at the call site. A callee that releases a value and then reinitialises the place (free(b->data); b->data = NULL;, v->items = realloc(v->items, n)) is summarised as freed,replaced (RFC 0008, Replaced values): the place itself is usable afterwards, but every copy of the old value the caller kept (int *old = v->items; grow(v); old[0]) is dead. Only what happens on a path that returns counts (free(g); exit(1); is no effect), and a callee that frees an element (free(history[len])) says so (freed,element): which element is not the caller’s to know, so calling it twice is not a double-free.
• Struct-by-value results (RFC 0008): a function that returns a record hands the caller its pointer fields (stores{result.data = fresh(free)}), so struct buf b = make(); ... owns b.data and must release it.
• Nullness (RFC 0008): the checker knows when a pointer is null (p = NULL) or may be null (the result of malloc, strchr, fopen, getenv, … or of any function in the program that can return null; a pointer compared with null whose null edge merged back). Dereferencing it, or passing it to a callee whose body dereferences the parameter without testing it, is a null-dereference. Every test idiom clears the fact on the non-null edge (if (!p) return;, if (p && p->x), p ? p->x : 0, while ((q = f()) != NULL), __builtin_expect), for the pointer and its copies; a callee’s outcome does too (if (!make(&p)) return -1; p[0] is clean when make returns *out != NULL). Pointers the checker knows nothing about (parameters, loaded fields, results of unchecked code) are trusted; WEAVEC_NULLABLE and WEAVEC_NONNULL say otherwise. Summaries record which parameters a function requires non-null (requires{s}) and the classes on which an out-parameter is non-null (notnull{*out}).
• Uninitialised pointers (RFC 0008): char *p; and the pointer fields of struct buf b; hold nothing until they are assigned; using them first is a use-of-uninitialized.
• Invalid releases (RFC 0008): free (or any releaser, or a consuming parameter) of a pointer to a stack or static object, a string literal, or the middle of an allocation (p + 1, the result of strchr) is an invalid-release.
• Integer facts and guards (RFC 0009): the checker knows the class (zero, positive, negative) and, when it can, the exact value of an integer local, parameter or field: from a constant assigned to it, from the edges of if (n == 0), if (n > 0), if (!c), if (n != 3) and every comparison with an integer constant, and from the case labels of a switch. A free, a move, a held resource or a null pointer established while such a fact holds is remembered under it, and the edge of a later test that contradicts the fact drops it: if (c) free(p); ... if (!c) use(p);, switch (n) { case 0: free(p); } ... switch (n) { case 1: use(p); } and char *p = NULL; if (n > 0) p = malloc(n); if (n <= 0) return -1; ... free(p); are clean. A branch whose condition the facts contradict (int c = 0; if (c) free(p);) is not taken. Reassigning the integer from an unknown value forgets the fact and weakens every guard that named it; supported arithmetic and computed tests also use typed ranges and bounded expressions (RFC 0017). Promotions, narrowing, _Bool conversion and mixed-sign comparisons follow the target’s C types. Full-width unsigned constants through 64 bits remain representable: unsigned x = -1 is UINT_MAX, and converting 256 to an eight-bit unsigned char produces zero. A fact about a converted expression is transferred to its source only when the transformation preserves it. Unknown or possibly invalid arithmetic cannot justify pruning a path.
• Argument-conditional summaries (RFC 0009): a callee whose free, move, store or returned value depends on a fact about its parameters is summarised with a when guard (param 1 freed(free) when param 3 zero, store param 0 *.msg = copy param 2 when param 2 nonnull, return fresh(free) when param 3 positive|negative), on a parameter, a field or dereference below one, or a global. At the call the guard is translated to the arguments (a constant or NULL argument decides it on the spot; a variable, a cast of one or n * 8 is looked up in the caller’s facts) and the effect is applied only when it is not refuted: l_alloc(ud, p, 8, 0) frees p and returns null, l_alloc(ud, p, 8, 16) does not free and returns a fresh block, b.noalloc = 1; release(&b); use(b.data) is clean when release frees only if (!b->noalloc), and gz_error(s, err, NULL) stores nothing. What survives translation stays attached to the record in the caller, where a later test may still refute it.
• Inferred noreturn (RFC 0009): a function whose every path ends in abort, exit, longjmp, a function declared noreturn or _Noreturn, an infinite loop, or a call to another such function is summarised never-returns, in the same file or across the program, and a call to it ends the path: if (bad) die("..."); use(p); is analysed on the good path only, nothing is leaked at the end of a block that is never left, and code after the call is dead. A function that returns on some path (void check(int ok) { if (!ok) die(); }) returns as far as the checker knows, and a call through a function pointer never returns only if every candidate never returns. No annotation is needed or added.
• Shared ownership and reference counts (RFC 0010): a resource on the books has a number of shares. A function that increments an integer field of its argument’s object (o->rc++, o->rc += 1, __atomic_fetch_add(&o->rc, 1, m), __sync_add_and_fetch(&o->rc, 1), in its own body or a callee’s) retains the argument, and the caller’s pointer gains a share. A function that frees the object when a decrement of that field reaches zero (if (--o->rc == 0) free(o), o->rc-- == 1, the atomic and __sync_ forms, or a helper such as dec_and_test(&o->rc) whose result says the count is zero) releases a share: the argument’s name is dead, and the object is gone only when that was the holder’s last share. A copy of a holder with a surplus takes one share with it (b = obj_ref(a); obj_unref(b); use(a) is clean), a copy of a holder with one share shares it (b = a; obj_unref(b); use(a) is a use-after-free), and a plain free kills every name. Releasing through a name this function never retained (a parameter it was handed) is a discipline, not a bug: the name is dead afterwards and nothing else changes. A share retained on a local and dropped is a leak when the field is a known count; a share retained on a parameter or global is the caller’s (increment param 0 *.rc in the summary). Libraries with no body in view are described with WEAVEC_RETAINS / WEAVEC_RELEASES.
• Per-outcome stores and facts (RFC 0010): a callee that stores an argument only on some outcome classes (int bag_put(struct bag *b, char *s) returning -1 when full) is summarised with stored <class> <path> lines, and on the edge where the caller rules those classes out the store is retracted: if (bag_put(b, s) < 0) free(s); is clean, and dropping s on that edge is a leak. Likewise what the callee left in the caller’s integer memory per class (fact negative param 0 *.filled =0) is known to the caller on the edge it takes.
• Stores out of sight (RFC 0010): a callee that copies its argument into memory its summary cannot name (a node it allocated and linked into the caller’s table: p->value = value; t->first = p;) is summarised param 1 escaped, and the caller treats the argument as it treats any value a callee stored a copy of: it has a second home, so it is not reported leaked and a share the call gave it is not lost. Wrappers pass the effect on, including through f(obj_ref(v)) (a result that is v or null resolves to v).
• Derived pointers (RFC 0011): a pointer is an object and an offset into it. &p->f, &p[3], p + 4, p->payload (an array member decaying) and (char *)p - offsetof(struct outer, in) are names for p’s object at a known offset, so free(container_of(i, struct outer, in)) frees what i was derived from, a callee that does so is summarised freed @-struct outer.in, a field pointer kept across free(p) is a use-after-free on its next use (not a conflicting-borrow at the free), and free(&o->in) or free(p + 1) names the offset in its invalid-release. Two field steps, an element step below a field, or a step by a variable amount make the offset unknown, which is still p’s object.
• Extents and bounds (RFC 0011): an allocation carries its size (malloc(n): n bytes; calloc(n, sz); realloc(p, n); a wrapper’s result: xmalloc(n) is summarised fresh extent=n), a variable and an array member their declared size, a string literal its length, and a WEAVEC_SIZED_BY(n) parameter n elements. An access p[i], *(p + i), (p + i)->f, or a library call’s buffer and length (memcpy, memset, fgets, read, snprintf, …) is compared with the extent: constant against constant outright; a symbolic index through what the path knows of it — the same counter (p[n] on malloc(n)), a relation learnt from a condition (i < n, i <= n, i >= n, also through one copy j = i), or a constant bound (i < 8) — and a pointer’s own offset is added (p = buf + 4; p[4] on eight bytes). A write to the index or the counter forgets what was known. A callee that accesses more of a parameter than its type promises (b[7] on char *b, for (i = 0; i < n; i++) b[i], for (i = 0; i < 8; i++) b[i], memset(b, 0, n)) is summarised with a requirement on that parameter’s extent (requires-extent{b: 8}, {b: n*4}), checked at every call against what the argument has and passed on through wrappers. RFC 0017 retains representable numeric conditions such as if (n > 4) b[4], the first accessed byte, and bounded product or minimum expressions. An unsupported condition makes coverage incomplete; dropping it cannot create an unconditional caller error.
• Strings (RFC 0012): beside its extent an object carries what is known of the string it holds — its length (a constant, or strlen(s) as a place of its own, or n when n = strlen(s)), or that it has no terminator — on the object and every exact alias of it. A literal or initialiser sets the length; strcpy, stpcpy, strcat, sprintf, strdup, fgets and snprintf leave a known or at least terminated string; strncpy with a source at least as long as the count, memset with a non-zero byte and memcpy from an unterminated source over the whole object leave none; a NUL store makes a string again; any other write forgets. The copies are checked as lengths (strcpy needs strlen(s) + 1, strcat needs what the destination holds plus the source plus one, sprintf at least the format’s literal bytes and one per conversion), the reads that seek a terminator (strlen, strcpy’s source, puts, %s) are reported on an object known to have none, and a copy that overflowed leaves the string unknown so it is reported once. A source of unknown length is not reported either way.
• Sized fields (RFC 0012): a pointer field whose object is counted by a sibling integer field. Declared with WEAVEC_SIZED_BY(cap), the field is loaded with cap elements of extent everywhere and stores into it are checked against cap. Undeclared, the pair is inferred: every store into the field anywhere in the program is a witness (v->items = malloc(n * sizeof *v->items); v->cap = n; says (items, cap, 4)) or a refutation (a store of an object no sibling counts, such as a caller’s pointer; a write to the count with no store into the pointer, such as v->n++); the pair holds when the witnesses agree on one count and nothing refutes it. A unit is analysed once more when its own stores confirm a pair its readers use, and the whole-program step does the same across units, so the inference needs no annotation and no particular order of files; what it costs is one more analysis of the functions that read the field.
• Offsets and lower bounds (RFC 0012): a relation between two integers carries an offset (i <= n - 1 is i < n; j = i + 1 makes a[j] under i < n one past), and a constant lower bound is kept beside the upper (i >= 8 decides buf[i] on eight bytes outright).
• Assumptions (RFC 0012): WEAVEC_ASSUME(expr) applies expr as the true edge of if (expr) would — a null test, a relation, a bound, a constant, an outcome of a call — and ends the path when the facts contradict it.
• Result provenance: a callee that returns one of its arguments or a pointer into one (strchr, next_of(n), &n->v) makes the result an alias or a borrow of that argument in the caller, so freeing the argument then using the result is reported.
• Aliases: q = p makes q and p names for the same object, so a free through either is a free of both. Reassigning a pointer separates it. So does a test (RFC 0006): on the edge where p != q holds the two are distinct (if (l == sentinel) return; free(l); use(sentinel); is clean), and on the edge where p == q holds they are the same object. != separates only pointers that hold the same value (q = p); q = p + 1 points into the same object and stays an alias.
• Borrows: &x, &s->f, array decay and &a[i] create a loan held by the pointer being assigned (mutable unless the pointer’s pointee type is const). Arguments to WEAVEC_BORROWED/WEAVEC_MUT parameters, and to parameters that a defined callee reads or writes through, borrow for the duration of the call. A loan ends when its holder is reassigned or is last used (RFC 0006): int *a = &n->v; *a = 1; free(n); is fine, free(n); *a = 1; is not. Loans held through a pointer (h->view = &n->v), by a global, or by a local whose address is taken last until the holder is reassigned. Copying a pointer that holds a loan into a longer-lived pointer is checked like creating the loan there. Two live pointers into one object, or writing an object another pointer views, are accepted by default; --exclusive-borrows rejects them as RFC 0001 does.
• Places: p, s.f, p->f, *pp, p->a->b, file-scope variables; all elements of an array share one place, written a[*] in diagnostics (*a for a pointer a). A free or move of an element remembers which element was named (RFC 0006): free(a[i]); a[i][0] = 0; and free(a[0]); free(a[0]); are reported, while for (i) free(a[i]); free(a);, free(a[0]); use(a[1]); and free(a[i]); a[i] = NULL; are clean. Assigning, incrementing or taking the address of the index variable makes the element unknown: it is then neither reported by element accesses nor cleared by element writes. An access without a subscript (*a, free(a) of the array’s owner) matches every element.
• Overwrites: a callee that writes an object wholesale (memcpy(root, &tmp, sizeof *root), or a defined function that writes through the parameter) makes every fact about the object’s fields stale, so free(root->string); memcpy(root, ...); use(root->string); is clean (RFC 0006).
• Annotations are checked: a body that frees a WEAVEC_BORROWED parameter is an annotation-mismatch; the annotation still governs what callers assume.
• Pointer identity: pointer arithmetic (p + 1, p++, &a[i]) and casts between pointer types ((char *)p, (void *)p) name the same object as the operand, so free(p); use(p + 1) is a use after free. Only a round trip through an integer loses identity, and what comes back is a raw pointer.
• Raw pointers and unsafe regions: a raw pointer is tracked (copies, comparisons and conversions to integers are fine) but dereferencing, releasing or handing it to an owning parameter outside a WEAVEC_UNSAFE region is an unsafe-operation. Unsafe regions are analysed like any other code with their diagnostics suppressed, so a free inside one is still a free afterwards.
• Unchecked calls: a call to a function with no body here, no annotations and no libc entry borrows its pointer arguments for the call, retains nothing, and returns an unknown value (this is what annotation-required reports). With --strict-externs the call is an unsafe-operation unless it is inside an unsafe region; its arguments are left alone and its pointer result is raw.

weavec --dump-analysis file.c -- <flags> prints the inferred places, lifetimes, exit state (including which places hold raw pointers, and why, which hold an owned resource, with its release family, and which are null, maybe-null or known non-null) and summary of every analysed function; with --whole-program it ends with the program database (every exported summary). weavec-cc writes each unit’s exported summaries to <object>.weavec in the same text form.

Constructors, returned fields and allocation-time sizes

RFC 0013 requires no new annotations. An inferred constructor describes the pointer fields of its returned or published object, including owned children, aliases of arguments, shared children and self-links. These facts also cross record returns and translation units. Existing diagnostics apply to them: a child access can be out-of-bounds, releasing its container can lose a child (leak), and using a field after releasing its referent is use-after-free. Known null, raw, borrowed, release-family and string facts retain their usual checks.

For example, after a helper returns a box whose data was allocated with malloc(4), the caller’s box->data[4] is out of bounds and free(box->data); free(box); releases both resources. Two fields initialized from the same allocation remain aliases; two constructor call sites create independent objects. Final values govern outputs: a field reset to null does not still hold its earlier allocation. A helper that fails without replacing an output leaves the caller’s incoming value and bounds intact.

An allocation uses the size’s value at allocation time. With size_t n = 4; char *p = malloc(n); n = 8;, a non-null p still has four bytes. Symbolic sizes can retain their relationship to an unchanged count copy after reassignment. Snapshot reuse in loops can lose precision, but cannot resize an older object to a later count.

--dump-analysis prints each heap description as complete or incomplete. These labels describe whether the bounded projection was truncated. A complete description is not a proof of safety: fields and extents can still be unknown. Projection follows at most eight steps and 128 field alternatives; more than eight alternatives for one cell widen it to unknown. The evaluation suite retains the original bug and clean populations; the RFC 0017 report records detection of both retained product and VLA cases, with 44/44 original bugs detected and 32/32 original clean cases.