Skip to content
PROJECT

Development history before 0.1.0

This historical snapshot preserves the hand-written notes from before the first public release, including implementation details and migration notes. It is not maintained for subsequent releases. Python Semantic Release creates CHANGELOG.md on the first public release and regenerates it thereafter.

All notable changes to WeaveC are documented here. The format is based on Keep a Changelog and the project follows Semantic Versioning once it reaches 1.0.

  • Publish versioned source archives and SHA-256 checksums to GitHub Releases after main passes CI. Conventional Commits select 0.x versions, stamp the CMake version and retain the hand-written changelog and migration notes.
  • Reuse context summaries according to observed function and global-fact dependencies, including missing callees and nested cache hits.
  • Retain parsed translation units and reusable CFG, scope and liveness data during whole-program analysis and compiler source replay. Bound ordinary runs without persistent reuse to one retained AST, and share owned call snapshots across CFG transfers. Release stale working databases and duplicate completed exports before constructing their replacements. Join spatial and alias facts directly and consume settled diagnostic-pass states while preserving the final exit state and analysis dumps. Schedule checked CFG work in reverse postorder with a reusable block order; preserve FIFO convergence and resource use throughout ordinary analysis.
  • Share immutable checked obligation entries and ledger snapshots on copy and across identical completed contexts through bounded weak indexes; separate semantic convergence from explanation wording and call routes.
  • Add optional --analysis-cache and --analysis-stats options, with matching compiler spellings. Settled checkpoints validate preprocessing, input bytes, commands, tool identity and imported facts before replaying diagnostics. Shared checkpoint tables preserve contracts too large for expanded transport; per-function statistics and partial snapshots expose unfinished work.
  • Add optional compact checked report version 3 and a compatible expansion script. Expanded version 2 remains the default.
  • Bind compiler objects to their preprocessing outcomes in sidecar format 16, closing stale-object validation when conditional includes become available. Rebuild older sidecars; Core summary format 15 remains unchanged.
  • Add frozen cache equivalence, invalidation, corruption, compiler-object and compact-explanation regression cases.
  • Fix summary parsing of widened Inside offsets (@~) in stores, returned values and heap descriptions, preserving facts in large checkpoints.
  • Preserve reachable checks after diverging loop cursors: checked nullness and branch facts require proven aliases, rather than possible equality on an earlier iteration.
  • Encode imported-fact keys losslessly, including spaced function-pointer type spellings and source paths, so independent units remain cacheable.

Practical checked memory contracts (RFC 0019)

Section titled “Practical checked memory contracts (RFC 0019)”
  • Infer initialized output intervals through nested fields, returned heap objects and output parameters, qualified by guards and returning outcomes. Preserve call-entry numeric values and initialization when helpers overwrite inputs; discard pending facts when their dependencies change.
  • Prove complete supported fill/copy loops and disjoint slices of one object. Keep pointer holders separate from pointee storage and retain unaffected evidence across complete helper calls.
  • Add checked string and positive-size reallocation models, initialized-prefix preservation, and zero-byte termination witnesses. Library trust remains explicit; allocation growth does not initialize the added tail.
  • Reuse bounded caller contexts for exact checked scalar inputs and fields. Keep recursive explanations stable without raising semantic analysis limits.
  • Transport conditional contracts and numeric outputs in summary/sidecar format 15 and checked JSON version 2. Rebuild objects with older sidecars.
  • Keep optional private-global output facts inside their translation unit, while rejecting lost entry requirements or premises of public outputs.
  • Add 32 frozen source cases, ten whole-program and compiler-object cases, and pinned Jansson buffer/UTF interface evaluations with adversarial callers.
  • Publish the validation report with repeated ordinary cost measurements and remaining whole-project checked limitations.
  • Keep propagated call provenance bounded without recursively escaping identities.
  • Require writable storage for direct and composed writes, rejecting writes to literals and cast-away const objects.
  • Add opt-in function and module selection, separate sufficient safety contracts, per-operation proof accounting and must-initialized memory facts.
  • Enforce callee contracts, including possible accesses in counted loops with early exits. Keep unknown bounds, uninitialized reads and unsupported semantics visible as checked failures.
  • Add WEAVEC_CHECKED, --checked, --checked-function, --checked-report, and corresponding -fweavec-* compiler options. Diagnostic demotion does not change checked acceptance. JSON reports record selection, requirements, unresolved operations, and transitive trust.
  • Transport checked contracts in summary/sidecar format 14. Bind compiler sidecars to object contents, source/header inputs and recorded commands; replay deferred external dependencies before linking.
  • C integer semantics and compositional spatial checking (RFC 0017): target widths through 64 bits, promotions, narrowing and _Bool conversions, full-width unsigned values, mixed-sign comparisons and modular unsigned arithmetic feed scalar guards, ownership effects, selected elements and sizes.

  • invalid-integer-operation (error) for definitely invalid supported arithmetic and nonpositive VLA dimensions. Possibly invalid arithmetic retains conservative facts; it cannot justify discarding a reachable path.

  • Bounded symbolic size expressions, allocation-time operand snapshots, checked add/subtract/multiply builtins and guarded multiplication, numeric returns and output values, and conditional access intervals through summaries. Supported unit-stride loops can export min(n, cap) bounds; early-exit and other unsupported loops do not infer must-requirements.

  • Call-entry numeric snapshots preserve allocation sizes and typed guards when a callee overwrites their input counts, including out-parameters and global fields. Integer dereferences and address-taking retain stored numeric values. Numeric output paths that alias the same caller cell are joined; contextual summaries retain the callee’s write order.

  • VLA declaration-time dimensions and sizeof values, allocated flexible-array tail extents, and counted-field inference that retains the C multiplication type. calloc and reallocarray retain checked-product failure semantics.

  • Spatial proven, violation and unresolved counts and unresolved reasons in --dump-analysis, independent of diagnostic suppression. Unsupported numeric representations and interface projections expose incomplete coverage.

  • Summary and sidecar format 13 for typed facts, expressions, numeric outputs and guarded access intervals. Rebuild objects carrying older sidecars. No new annotation spellings or verification mode are introduced.

  • Twelve separate bug/clean regression pairs and a hardened recall runner that rejects process failures even after expected reports were printed.

  • An RFC 0017 validation report and reproducible corpus results: 900/900 tests pass normally and under ASan/UBSan, original fixed detection improves from 42/44 to 44/44 with 32/32 clean cases, and recall remains 67/67. Three runs per binary show median corpus time growing from 141 to 336 seconds and peak memory growing 19%, beyond the RFC targets. Three new Jansson false positives and incomplete coverage are documented.

  • Monotone recursive summary joins prevent typed guard projection from oscillating between summaries. Packed numeric-write sets retain the same facts with less state-copy overhead. Abstract range endpoints alone no longer fabricate reachable out-of-bounds witnesses.

  • Compositional call checking (RFC 0016): helpers are checked under the caller’s pointer, storage and reference-share relationships, retaining statement order through aliased parameters, fields, globals and selected elements. Release-before-use and repeated releases are diagnosed inside the helper; write-before-release and supported replacement remain clean.

  • Bounded memory contexts combined with actual callback targets, entry facts, final summaries, nested call notes and unsafe-reporting state. Contexts travel across translation units and compiler link analysis, including annotated definitions and locally complete object files.

  • Summary and sidecar format 12, with strict context validation and global remapping. Rebuild objects carrying earlier sidecars. Unsupported context projections and exhausted limits expose analysis-incomplete coverage.

  • Twelve additional fixed bug/clean pairs and Core, checker, whole-program and compiler regression tests. The RFC 0016 validation report records the fixed evaluation and the full diagnostic changes on the pinned corpus.

  • Array and container ownership (RFC 0015): selected pointer/record cells, stable scalar index snapshots, independent initialization and nullness, nested arrays, callback cells and retained-share copies.

  • Simultaneous complete array copies and overlapping moves, sparse symbolic range snapshots, final range summaries and returned containers. Reallocation preserves child pointer values while invalidating the original storage.

  • Proved contiguous cleanup and simple fill loops, with bounded initialization and release intervals. Unsupported selections and range compositions expose analysis-incomplete without discarding known release history.

  • Summary and sidecar format 11 for selected paths, range copies, fills and releases. Rebuild objects carrying earlier sidecars.

  • Twelve additional fixed bug/clean pairs, exact array diagnostics, whole-program and compiler-sidecar integration tests, and a corpus manifest with pinned Lua, Jansson, linenoise, cJSON and log.c revisions.

  • Pointer identity and precise call effects (RFC 0014): bounded sets of actual callback targets flow through assignments, fields, copies, returns and out-parameters. Callback helpers are specialized with their actual targets while retaining the body’s userdata associations and statement ordering. Unknown callbacks remain checking boundaries even when unrelated functions of the same type exist in the program.

  • Pointer equality and inequality predicates on ownership effects, including argument snapshots and cross-file summaries.

  • Complete pointer and compatible record copies through memcpy and memmove, including pointer aliases, callback targets and reachable state.

  • Record-layout metadata on summary paths and a stable analysis-incomplete warning for unsupported memory copies, incompatible views and exhausted analysis limits. Dumps show callback targets, binding contexts and coverage.

  • Summary and sidecar format 10, including callback contexts and global target values. Rebuild object files carrying older sidecars.

  • Paired RFC 0014 evaluation cases and a pinned corpus subset. The corpus runner records process failures, timeouts and optional peak memory, rejects empty runs and source-revision mismatches, and does not update a baseline from a failed analysis.

  • Analysis unit-test fixtures now reject Clang parse errors. Invalid existing fixtures were corrected; macOS SDK discovery no longer leaks Xcode startup messages into checker output.

  • Interprocedural heap postconditions (RFC 0013): constructors preserve owned children, argument aliases, shared children, self-links, bounds, null/raw fields and string facts through pointer returns, record returns and out-parameters. The same facts cross translation units and compiler sidecars; freeing a returned container now reports its unreleased children.

  • Allocation-time size identities: reassignment of a size variable no longer erases a known constant extent; bounded symbolic snapshots preserve useful relations to copies of the original count.

  • Final output values are distinguished from intermediate stores and incoming pointer values. Replacement invalidates old aliases, failed replacements restore the incoming pointer and its bounds, and pointer extraction retains the removed value. Lazy initialization preserves an existing object’s state.

  • A fixed evaluation set, including known misses, with separate counts for detected bugs, clean programs, unexpected reports, parse failures, tool failures and timeouts (scripts/evaluate.py, part of CTest).

  • Heap coverage in --dump-analysis: descriptions have explicit depth and alternative limits; truncated descriptions are printed as incomplete. These fields were introduced in format 9; the current format is 13.

  • Reviewed corpus measurements for RFC 0013, including the substantial increase in false positives on Lua’s GC and broad callback candidate sets. The corpus notes record the precision cost alongside the new capabilities.

  • Initial project scaffolding: CMake build with presets, LLVM/Clang discovery, strict warnings, sanitizer and LTO options, install/export rules and CPack.

  • weavec::Core: Clang-independent ownership lattice (OwnershipKind), lifetime constraints, loan tracking (BorrowState), move tracking (MoveTracker) and a frontend-neutral diagnostics interface.

  • weavec::Analysis: annotation recognition and a first path-insensitive local ownership checker reporting use-after-free, double-free, invalid-annotation and (opt-in) annotation-required.

  • weavec::Frontend: Clang ASTFrontendAction, diagnostics bridging to Clang’s DiagnosticsEngine, resource-directory discovery.

  • weavec command-line tool built on libTooling (weavec file.c -- <flags>), with --report-unannotated and --analyze-headers.

  • weavec.h annotation header: WEAVEC_OWNED, WEAVEC_BORROWED, WEAVEC_MUT, WEAVEC_UNSAFE, WEAVEC_ENABLED.

  • GoogleTest unit tests and lit/FileCheck integration tests.

  • GitHub Actions CI (Linux ASan/UBSan + Release, macOS Release, clang-format, cmake-format, clang-tidy, CodeQL), Dependabot, issue and PR templates.

  • Project documentation: architecture, annotations reference, developer guide, roadmap.

  • RFC process for changes to the model, checker rules, annotations and diagnostics (docs/rfcs/), with RFC 0001 (ownership model), RFC 0002 (sound intra-procedural checking), RFC 0003 (signature inference) and RFC 0004 (unsafe boundaries).

  • Sound intra-procedural checking (RFC 0002): a forward dataflow over clang::CFG replaces the path-insensitive AST walk, so loops, switch fall-through, goto and short-circuit operands are analysed on every path and each problem is reported once.

  • Pointer copies are tracked as aliases (core::AliasRelation): freeing through one name frees every name, and the note says which (freed here (through 'q')).

  • Structured places: s.f, p->f, *pp, nested field paths, and one summary place per array (a[*]).

  • Allocator and release recognition (malloc, calloc, realloc, strdup, strndup, aligned_alloc, free, WEAVEC_OWNED returns/parameters), with the realloc failure idiom (if (!q) free(p)) accepted.

  • New diagnostics: use-after-move (owned pointer passed to a WEAVEC_OWNED parameter or to realloc, then used), conflicting-borrow (two live borrows that conflict, or writing/freeing/moving a borrowed object) and lifetime-too-short (a pointer to a local stored somewhere that outlives it, or returned).

  • Borrows from &x, &s->f, array decay and WEAVEC_BORROWED/WEAVEC_MUT arguments; loans are mutable unless the pointer’s pointee is const.

  • weavec --dump-analysis prints the inferred places, lifetimes and exit state of every analysed function.

  • Signature inference (RFC 0003): every function definition in a translation unit gets a core::FunctionSummary (effects on parameters, paths under them and globals; stores into caller-visible memory; return-value provenance), inferred bottom-up over the call graph with a fixpoint inside recursive cycles, and applied at every call site. node_free(n); n->v, buf_destroy(&b); b.data[0], out-parameters, helpers that free globals and wrappers of wrappers are now checked without annotations.

  • Shipped summaries for the C standard library (malloc family, str*, mem*, stdio, strtol, getenv, …), including which results alias which arguments (strchr, strtol’s end pointer) so real headers need no annotations.

  • annotation-mismatch (error): a definition’s body contradicts its own WEAVEC_OWNED/WEAVEC_BORROWED/WEAVEC_MUT annotation (frees or writes through a borrowed parameter, moves a WEAVEC_MUT one, returns a borrow from a WEAVEC_OWNED result, …). Callers keep trusting the annotation.

  • annotation-required is on by default at the external boundary: the first call to a function with no definition here, no annotations and no libc entry warns once per callee (system headers exempt). --strict-externs makes it an error. With --report-unannotated, exported functions get one warning per unannotated pointer position carrying a fix-it that inserts the inferred annotation.

  • core::Diagnostic carries FixItHints, bridged to Clang so -fdiagnostics-parseable-fixits and editors can apply them.

  • --dump-analysis prints a summary: line per function.

  • scripts/corpus.py: runs weavec over real C projects (scripts/corpus/projects.json), tallies diagnostics per id and compares with scripts/corpus/baseline.json; a weekly Corpus workflow runs it.

  • TranslationUnitAnalyzer (Analysis) and SummaryStore as the public entry points for whole-TU analysis; FunctionAnalyzer::analyze now takes the store.

  • Raw pointers (RFC 0004): a pointer cast from an integer, declared WEAVEC_RAW, loaded through another raw pointer, or handed out as raw by a callee is tracked as raw (core::RawTracker, AnalysisState::raw, ValueSource::raw()). Dereferencing it, releasing it, passing it to an owning or dereferencing parameter, or asserting a safe kind for it outside a WEAVEC_UNSAFE region is the new unsafe-operation error, with a note saying why the pointer is raw. Copying, comparing and converting it back to an integer are fine anywhere.

  • WEAVEC_RAW annotation for pointer parameters, returns, variables, fields and function-pointer types (“no ownership guarantee”). weavec.h is at header version 0.2.

  • Laundering (RFC 0004): inside a WEAVEC_UNSAFE region, assigning a raw pointer to a place declared WEAVEC_OWNED/WEAVEC_BORROWED/WEAVEC_MUT or returning it from a function whose return type is so annotated asserts that kind, so pointers can be brought back into the model at one explicit point (WEAVEC_UNSAFE { n = (struct node *)handle; } free(n);).

  • Calls through function pointers (RFC 0004) are checked: the signature comes from ownership annotations on the function-pointer type (typedef void (*dtor_t)(void *WEAVEC_OWNED);, fields, parameters), else from the join of the summaries of every function of that type whose address is taken in the translation unit (ops.drop = node_free;, qsort(..., cmp)). Callbacks are analysed before their callers. Pointers with neither get one annotation-required warning per function-pointer type.

  • POSIX and common GNU/BSD functions in the shipped library table (about 490 entries, up from 85): <unistd.h>, <fcntl.h>, <sys/stat.h>, <dirent.h> (opendir/closedir/readdir), <stdio.h> extensions (getline, getdelim, asprintf, popen/pclose, fmemopen, open_memstream), <stdlib.h> extensions (posix_memalign, reallocarray, realpath, mkstemp, qsort_r), <string.h> extensions (strtok_r, strsep, stpcpy, strlcpy, memmem, …), <time.h>, <sys/mman.h> (mmap/munmap), <pthread.h>, <sys/socket.h>, <netdb.h> (getaddrinfo/freeaddrinfo), <arpa/inet.h>, <dlfcn.h>, <regex.h>, <signal.h>, <sys/wait.h>, <poll.h>, <pwd.h>, <grp.h>, <iconv.h>, <glob.h>, <wchar.h> and more.

  • --dump-analysis prints the raw component of the exit state (raw{r@3:13 integer-cast}), raw as a place kind and as a value source.

  • core::FunctionSummary::inferredReturnKind reports Raw; --report-unannotated offers WEAVEC_RAW for a result inferred raw.

  • SummaryStore::lookupIndirect, addAddressTaken, candidatesFor; analysis::collectFunctionTypeAnnotations; TranslationUnitAnalyzer:: collectAddressTaken.

  • Whole-program analysis (RFC 0005): the unit of analysis is the program, not the translation unit. Every unit exports the summaries of its external-linkage definitions and address-taken functions; a ProgramDatabase (Analysis) collects them and SummaryStore consults it between a unit’s own inference and the libc table, so node_free(n); n->v is caught when node_free is defined in another file, a program’s own strdup is checked against its own body, and a callback installed in one file is joined into the signature of the function-pointer type it is called through in another. Units are analysed dependencies-first by strongly connected component (core::stronglyConnectedComponents, Core/Scc.h); mutually dependent units iterate to a fixpoint.

  • weavec --whole-program [files] -- <flags> (or -p build/ for every file of a compilation database) analyses the files as one program; --dump-analysis then ends with the program database.

  • weavec-cc, a drop-in C compiler: Clang’s driver plans the jobs, each -cc1 runs in-process with WeaveC’s consumer multiplexed beside Clang’s code generation (one parse; a WeaveC error fails the compile). The compile step writes the unit’s exports, its cc1 command and the diagnostics it reported to <object>.weavec; the link step reads the sidecars of the objects on the link line, re-analyses the units whose results depend on other units, reports what needs two files (once), and refuses to link on an error. Objects without a sidecar are unknown code; a sidecar older than its object is ignored with a warning; sidecars of one-step builds (weavec-cc a.c b.c -o prog) are read and removed with the temporaries. -cc1as and other jobs are delegated to clang (WEAVEC_CLANG, the configured WEAVEC_CLANG_EXECUTABLE, or PATH).

  • Driver flags: -fweavec/-fno-weavec, -fweavec-strict, -fweavec-report-unannotated, -fweavec-analyze-headers, -fweavec-dump-analysis, -fweavec-link/-fno-weavec-link. Warning control for both tools (frontend::DiagnosticControl): -Wno-weavec-<id> (warnings only), -Wweavec-<id>, -Wno-error=weavec-<id>, -Werror=weavec-<id>, -Wno-weavec, -Wno-error=weavec, -Werror=weavec. Disabling an error is refused with a message naming the -Wno-error= form.

  • core::FunctionSummary text format (Core/SummaryIO.h: printSummary/parseSummary, SummaryFormatVersion), Clang-free and round-trip tested; globals are spelled by name through callbacks. core::FunctionSummary::remapGlobals. core::diag::All, isKnown, isWarningByDefault.

  • analysis::UnitExports, ExportedFunction, functionTypeKey, ProgramDatabase; SummaryStore::setDatabase, SummarySource::Program, isAddressTaken, unknownCalleeNames, unknownIndirectTypeKeys; TranslationUnitAnalyzer::setDatabase, discover(), exports(); AnalysisOptions::deferBoundary.

  • frontend::ProgramAnalysis (over an abstract ProgramUnit; CompilationDatabaseUnit), frontend::Sidecar.h (UnitRecord, readSidecar/writeSidecar, weavec-summaries 1), frontend::Driver.h (DriverOptions, runDriver, runCc1), createWeaveCConsumer, FrontendOptions::{database, alreadyReported, boundaryOnce, silent, discoverOnly, onResult}, UnitResult.

  • WeaveCFrontendTests unit-test binary; test/WholeProgram/ and test/Driver/rfc0005-*.c lit suites.

  • scripts/corpus.py: "whole_program": true projects are analysed as one program (--local-whole-program for --local); cJSON-program and linenoise-program added to the corpus, with triage in scripts/corpus/README.md.

  • Precision (RFC 0006). Loans end at the last use of their holder, not at the end of its scope: a backward liveness pass over the CFG expires the loans held by dead locals before each element, so char *p = buf; use(p); buf[0] = 0; and int *a = &n->v; *a = 1; free(n); are clean while free(n); *a = 1; is still cannot free 'n' while it is borrowed. Loans held through a pointer, by a global or by an address-taken local last until the holder is reassigned (BorrowState::expireHolders).

  • Condition facts on CFG edges (RFC 0006): p == q / p != q unite or separate the two pointers on the edge where the test holds, so if (l == sentinel) return; free(l); use(sentinel); is clean; != separates only exact aliases. AliasRelation records per edge whether two places hold the same value or point into the same object (unite(a, b, exact), separateExact, isExact, edge); pointer arithmetic makes a copy interior (ValueOrigin::interior, ValueSource::interiorCopy, printed interior <path>), and the libc table says which results are the argument itself (memcpy, strcpy, fgets, getcwd, …) and which point into it (strchr, strstr, strtok, bsearch, readdir, the strto* end pointers, …).

  • Element witnesses (RFC 0006): a[*] is still one place, but a move record remembers which element was named (core::ElementWitness: whole, a constant, a variable, or unknown) and only an access with a matching witness is a use of it. free(a[i]); a[i][0] = 0; and free(a[0]); free(a[0]); are reported; for (i) free(a[i]); free(a);, free(a[0]); use(a[1]);, free(a[i]); a[i] = NULL; and free(a[i]); use(a[j]); are clean. Writing to, incrementing or taking the address of the index variable makes its witnesses unknown (MoveTracker::forgetWitness). *a on an array is a[0].

  • Outcome-conditional summaries (RFC 0006): a callee that frees or moves an argument only on the paths returning some class of value (null / nonnull, zero / positive / negative) is summarised per class (core::Outcome, FunctionSummary::outcomes, addOutcome, consumesUnconditionally), and a caller’s test of the result (if (!q), q == NULL, rc != 0, rc < 0, rc == -1, (rc = f(p)) == 0, …) retracts the consumption on the edge where it did not happen. int rc = try_take(p); if (rc != 0) free(p); is clean and if (rc == 0) use(p); is a use-after-move; wrappers around realloc (if (!q) return NULL; return q;) and around error-returning functions inherit the conditional behaviour, across units too. realloc’s null edge is now this mechanism (AnalysisState::pending, PendingOutcome, AnalysisState::consumed; reallocLike/isRealloc are gone). Summary text format version 2: outcome <class>, outcome <class> <path> <flags>, interior <path>; sidecar format version 2 (weavec-summaries 2); --dump-analysis prints the classes (outcome zero{n: freed} outcome negative{}).

  • A callee’s written effect forgets every fact below the written place (RFC 0006), so free(root->string); memcpy(root, &tmp, sizeof *root); use(root->string); is clean and the summary of such a body no longer claims the field is freed. Fortified __builtin___memcpy_chk-style variants of the mem*/str* copy functions share their entries.

  • --exclusive-borrows (weavec) / -fweavec-exclusive-borrows (weavec-cc), AnalysisOptions::exclusiveBorrows: enforce RFC 0001’s exclusivity between borrows (see Changed).

  • zlib (15 units) and Lua (34 units) added to the corpus as whole programs. zlib is clean apart from two callback boundaries; every Lua report is triaged in scripts/corpus/README.md. The corpus baseline now has no use-after-free outside Lua, no conflicting-borrow outside Lua and two double-free outside Lua (down from 15, 4 and 10).

  • Resource lifecycle (RFC 0007). Every allocation, WEAVEC_OWNED parameter and fresh result puts a resource on the function’s books (core::ResourceTracker, AnalysisState::resources, ResourceRecord), and the checker reports what happens to it:

    • leak (new, warning): the resource’s last holder goes out of reach (return, scope end, the statement after its last use, a value that is never read) without it having been released, moved, returned, stored into caller-visible memory, handed to unknown code or cast to an integer; also '<p>' is leaked: it is overwritten without being released, '<b>->p' is leaked when '<b>' is freed, result of '<f>' is leaked for a discarded allocating call. Copies share one record and one report; a callee summarised from its body that records no effect on a pointer parameter is trusted not to retain it; the null edge of a test of the holder owns nothing (through __builtin_expect and (c) != 0 too); a block ending in a noreturn call is not a death point, nor is the edge into one; a value stored below a pointer whose object nobody here owns or names (box = lua_touserdata(L, 1); box->buf = malloc(n)) escapes; a resource kept by a global or static local is not a leak.
    • mismatched-release (new, error): every allocator in the shipped table belongs to the family of its releaser (malloc/strdup/reallocfree, fopenfclose, opendirclosedir, getaddrinfofreeaddrinfo, mmapmunmap, popenpclose, …), and releasing a resource of one family with a function of another (free(fopen(...)), fclose((FILE *)malloc(8)), realloc(f, n) on a FILE) is reported, through wrappers defined in the program and across units. Inferred summaries carry the family (fresh(fclose), freed(free), moved(free); ValueSource::family, PlaceEffect::family, FunctionSummary::freshReturnFamily).
    • WEAVEC_OWNED on a struct field is now enforced: free(b) with b->p neither freed, moved, tested nor nulled is a leak of b->p, for objects that came from outside (a parameter, a global, a load). A field this function stored an owned value into is checked the same way without the annotation (b->data = malloc(8); free(b);), as are array elements (a[0] = strdup("x"); free(a);).
    • Per-outcome null facts (FunctionSummary::nullOn, PendingOutcome:: nullOn): a constructor that reports failure through its result (int make(char **out) { *out = malloc(n); return *out != NULL; }, or if (*out == NULL) return -1;) is summarised with the classes on which *out is null or holds nothing the callee stored (the guard returns before the store, if (strm == NULL) return Z_STREAM_ERROR;), so if (!make(&s)) return; free(s); and err = init(&s); if (err != 0) return err; are clean (RFC 0007, Per-outcome null stores).
    • weavec.h header version 0.2 → 0.3 (documentation of WEAVEC_OWNED on fields). -Wno-weavec-leak disables the warning; -Werror=weavec-leak promotes it.
    • Summary text format version 2 → 3: freed(<family>), moved(<family>), fresh(<family>) and null <class> <path> lines; sidecar format version 3 (weavec-summaries 3). --dump-analysis prints the exit state’s resources (owned{p@3:14 allocated free}) and the families in summaries; the program dump uses the same spellings.
  • Pointer validity (RFC 0008). Three new diagnostics, all errors by default (lower with -Wno-error=weavec-<id>; they cannot be disabled):

    • null-dereference: a pointer that is null or may be null on some path is dereferenced (dereference of '<p>', which may be null / which is null), or passed to a callee that dereferences its parameter without testing it ('<p>', which may be null, is passed to '<f>', which dereferences it). The new core::NullTracker (AnalysisState::nulls) knows null constants, the results of every allocator and searching function in the shipped table (malloc, strchr, fopen, getenv, fgets, realpath, …), the results and out-parameter stores of every function in the program whose body can produce null, declared WEAVEC_NULLABLE places, and pointers whose null test merged back. Every test idiom (if (!p), p == NULL, &&/||/?:, while ((q = f())), __builtin_expect) clears the fact on the non-null edge 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 are trusted, a redundant retest of a pointer already known non-null does not make it maybe-null (cJSON’s can_access_at_index), (T *)0 is a null constant like NULL (zlib’s Z_NULL casts), and a call into unchecked code forgets what it knew about the storage it was handed by address (a callback filling linenoiseCompletions lc = { 0, NULL }). A callee’s failing outcome class makes a place null only when the callee can have left null there: the RFC 0007 null{...} entry for a fresh store that did not happen on that class (if (grow(b, n) == -1)) still drops the caller’s resource record but no longer says the buffer is null (linenoise’s linenoiseEditGrow, cJSON’s ensure, zlib’s gz_init). Summaries carry requires{s} (the parameters a function dereferences untested; every r/w parameter of the shipped table except those documented to accept NULL) and notnull{*out} per outcome class; returns{...} lists null.
    • use-of-uninitialized: a pointer variable, or a pointer field of a record variable, declared without an initialiser is read, dereferenced, copied or released before it is assigned (use of '<p>' before it was initialized). core::MoveReason::Uninitialized; any assignment, a callee’s store, a mutable borrow for a call or memset initialises it.
    • invalid-release: free (or any releaser, or a consuming parameter) of a pointer to a stack or static object ('<p>' is released but points to '<x>', which is not a heap object), to a string literal, or into the middle of an allocation (p + 1, strchr(p, c): '<p>' is released but does not point to the start of its allocation; ResourceRecord:: interior). String literals are borrows of a static synthetic place.
    • WEAVEC_NULLABLE and WEAVEC_NONNULL (weavec.h header version 0.3 → 0.4): on parameters, return types, variables and fields; neither says anything about ownership. Both on one declaration is invalid-annotation.
    • Replaced values: a callee that releases a caller-visible value and then reinitialises the place (free(b->data); b->data = NULL;, v->items = realloc(v->items, n)) now records the consume (freed,replaced / moved,replaced), so a caller’s copy of the old value (int *old = v->items; grow(v); old[0]) is a use-after-free / use-after-move while the place itself stays usable (RFC 0008, Replaced values). This closes the soundness hole RFC 0003’s exit-state rule left open and replaces RFC 0007’s Deliberately not caught entry for it. Only consumption on a path that returns counts: lua_close(L); exit(1); does not free L->l_G as far as callers are concerned.
    • Element consumes: a callee that frees an element (free(history[len])) says so (freed,element), and the caller applies the consume with an unknown element witness (RFC 0006), so two such calls in a loop are not a double-free of *history.
    • Struct-by-value results: a function returning a record hands the caller its pointer fields through the new result summary root (stores{result.data = fresh(free)}), so struct buf b = make(); owns b.data and its leak is reported.
    • Summary text format version 3 → 4: the replaced and element flags, requires N, notnull <class> <path> and the result root; sidecar format version 4 (weavec-summaries 4). --dump-analysis prints nulls{p@3:14 maybe-null, q nonnull} in the exit state, uninitialized moves, interior resources, and the new summary words.
  • Value-conditional behaviour (RFC 0009). No new diagnostic; three sources of false positives that every real code base hits are closed:

    • Integer facts and guards: the new core::ScalarTracker (AnalysisState::scalars) knows the class (zero, positive, negative) and, when it can, the exact value of an integer local, parameter or field, from constants assigned to it, from the edges of every comparison with an integer constant (n == 0, n > 0, !c, n != 3) and from switch cases. Every move, held resource and null record carries the PlaceGuard of the path that created it, and a later test that contradicts the guard drops the record on that edge: if (c) free(p); ... if (!c) use(p);, a second switch on the same opcode, and char *p = NULL; if (n > 0) p = malloc(n); if (n <= 0) return -1; ... free(p); are clean; int c = 0; if (c) free(p); does not take the branch at all. Writing the integer forgets the fact and weakens every guard that named it; a fact about memory behind a pointer never prunes an edge (aliasing), only the guards.
    • Argument-conditional summaries: a consume, store or return alternative that happens only under a fact about the callee’s entry values is summarised with a when guard (param 1 freed(free) when param 3 zero, return fresh(free) when param 3 positive|negative, store param 0 *.msg = copy param 2 when param 2 nonnull; at most MaxGuardConjuncts conjuncts, never on a path the callee wrote). At the call the guard is translated to the arguments — a constant or NULL argument decides it, a variable is looked up in the caller’s facts — and the effect applies only when it is not refuted; what survives stays on the record in the caller. l_alloc(ud, p, 8, 0) frees p and returns null, l_alloc(ud, p, 8, 16) returns a fresh block and keeps p; release(&b) with b.noalloc = 1 frees nothing; gz_error(s, err, NULL) stores nothing. SummaryStore keeps neverReturns and guards across the per-type join and the program database. A value gone at the callee’s exit only under a guard (if (b == NULL) finish(L); else append(L, b);) is an unreplaced consume under that guard, not an unconditional one, so a caller whose argument refutes it is not told its stack was freed (Lua’s str_writer under dumpBlock).
    • Inferred noreturn: a function whose every path ends in abort, exit, longjmp, a declared noreturn/_Noreturn callee, an infinite loop or another such function is summarised never-returns, in the same unit and across the program; a call to one ends the block (the liveness pass agrees, so nothing is leaked at the end of a block that is never left) and code after it is dead. A function that returns on some path returns; a call through a function pointer never returns only if every candidate never returns.
    • Summary text format version 4 → 5: the never-returns line and the optional when <path> <fact> [and ...] guard on effect, outcome, store and return lines (fact ::= =<integer> | <class>[|<class>]*); sidecar format version 5 (weavec-summaries 5). --dump-analysis prints scalars{n =0, m positive|negative} in the exit state, when[c =0] on guarded moves, resources and nulls (otherwise-nonnull on a null record that is non-null when its guard fails), never-returns and the when[...] clauses in summaries.
    • Corpus (scripts/corpus/README.md): the l_alloc family of Lua reports (double-free, use-after-free, conflicting-borrow, invalid-release and the function-pointer leaks), the luaL_error null-dereferences, cJSON’s p.buffer leak, zlib’s state->msg leaks and the noalloc/ noreturn correlations RFC 0006 and RFC 0008 listed under Accepted false positives are gone.
  • Shared ownership (RFC 0010). The one-owner model gains shares, so reference-counted objects, the most common way C shares an object, are checked instead of misreported:

    • Reference counts are inferred from the bodies that keep them: 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)) retains it (increment param 0 *.rc); one that frees the object when a decrement of the field reaches zero (if (--o->rc == 0) free(o), o->rc-- == 1, the atomic and __sync_ forms, or a helper like dec_and_test(&o->rc)) releases a share (param 0 freed(free),share, count param 0 *.rc). The caller’s ResourceRecord counts shares: obj_ref(a) adds one, a copy of a holder with a surplus takes one (b = obj_ref(a) makes b its own share, an alias of a for frees but not for releases), obj_unref takes one and kills the name only when it was the last. A share released on a name this function never retained (a parameter) is a discipline: the name is dead, other shares live on. A plain free still kills every alias.
    • New messages on existing ids: use of 'p' after its reference was released / reference released here, 'p' is released twice / previously released here, and the leak note reference taken here for a share that is retained and dropped (void f(struct obj *o) { struct obj *p = o->next; obj_ref(p); }). A leak of a share is reported only through a known count: a field some function in the program releases through, or one annotated WEAVEC_REFCOUNT; incrementing a length is not a leak.
    • Per-outcome stores: a callee that stores an argument only on some outcome classes (bag_put returning -1 when full) is summarised stored zero param 0 *.items[] / stored negative and the caller retracts the store on the classes it rules out, so if (bag_put(b, s) < 0) free(s); is clean and the failure edge that drops s is a leak.
    • Per-outcome integer facts: what a callee left in the caller’s integer memory per class (fact positive param 0 * =0 for dec_and_test, fact negative param 0 *.filled =0) is known after the call on the edge the caller takes.
    • Annotations WEAVEC_RETAINS and WEAVEC_RELEASES (pointer parameters: a library’s g_object_ref/g_object_unref with no body in view; a returning ref’s result is a copy of its argument), WEAVEC_REFCOUNT (an integer field is a count) and WEAVEC_OWNED_BY(f) (the release family of a WEAVEC_OWNED result or parameter, closing RFC 0007’s open item); weavec.h 0.5. WEAVEC_OWNED_BY without WEAVEC_OWNED, or WEAVEC_RETAINS with WEAVEC_RELEASES on one declaration, is invalid-annotation.
    • Stores out of sight: a callee that copies its argument into memory its summary cannot name (p->value = value in a node it allocates and links into the caller’s table) says param 1 escaped, wrappers pass it on (through table_set_new(t, obj_ref(value)) too: a param i root now resolves through a value that is a copy or null), and the caller neither reports the argument leaked nor loses the share it just took. Every container insert of an owned value (table_set(t, o) with o from malloc) was a false leak before.
    • Summary text format version 5 → 6: the share and escaped flags on effects and the increment, decrement, count, stored and fact lines; sidecar format version 6 (weavec-summaries 6) with count-field <key> lines. --dump-analysis prints shares and the count field on resources, released moves, escaped effects, increments{}, decrements{}, counts{} and per-class stored{} / facts{} in summaries, and count-field lines in the program database.
    • The whole-program fixpoint (RFC 0005) re-analyses a member of a cyclic group only when the exports it imports changed since its last run. Lua as one program (release build, same machine): 3 min 16 s before this release, 2 min 16 s with shares and the fixpoint change, 3 min 22 s once escaped effects are applied at every call; the last figure is the quietest of several runs on a machine that was otherwise busy.
    • Corpus: jansson (reference-counted JSON, analysed as one program) joins scripts/corpus/projects.json; {support} in a project’s arguments names scripts/corpus/support/<project>, for headers a checkout’s build would generate.
  • Spatial safety (RFC 0011). A pointer is now an object and an offset into it, objects have a size, and accesses are checked against it:

    • Derived pointers: &p->f, &p[3], p + 4, p->payload (an array member decaying) and (char *)p - offsetof(struct outer, in) are the same object at a known offset (core::PointerOffset: zero, a constant number of elements, a field, or unknown), replacing the boolean interior flag on alias edges and resources. container_of round trips (free(container_of(i, struct outer, in)) frees i’s object, release(&o->in) on a wrapper that does so is a double-free of o), q != p separates two derived pointers, and a field pointer kept across free(p) is a use-after-free on its next use (it was a conflicting-borrow at the free). invalid-release names the offset (points 4 elements past the start / points to field 'in'). Summaries record the offset a parameter was consumed at (param 0 freed(free) @-struct outer.in) and the offset of a returned copy (return copy param 0 @+struct list.next).
    • Extents: malloc(n), calloc(n, sz), realloc(p, n) and every function in the program that returns a fresh allocation (return fresh extent=n), locals, arrays and array members of declared size, string literals and WEAVEC_SIZED_BY(n) parameters carry a size (core::Affine: a constant, or scale * place + constant), kept by core::SpatialTracker beside the resource books.
    • Relations: core::RelationTracker records i < n, i <= n, i >= n, i == n between integer places from condition edges (through one copy j = i), and a constant upper bound (i < 8); a write to either side forgets them.
    • New diagnostic out-of-bounds (error): p[i], *(p + i), (p + i)->f and the buffer/length pairs of the shipped table (memcpy, memmove, memcmp, memset, memchr, strncpy, strnlen, fgets, snprintf, vsnprintf, strlcpy, strlcat, bzero, read, pread, recv, write, send, getcwd, readlink) are checked against the object’s extent: constant against constant, a symbolic index through the same counter (p[n] on malloc(n)), a relation ('i' may equal 'n' under i <= n, 'i' is at least 'n' under i >= n), or a constant bound ('i' may be 7 in an object of 4 bytes under i < 8); the pointer’s own offset is added (p = buf + 4; p[4]); accesses before the start are reported too. Nothing is reported when the checker cannot relate the index to the extent.
    • Extent requirements in summaries: a callee that accesses more of a parameter than its type promises (b[7], for (i = 0; i < n; i++) b[i], memset(b, 0, n)) is summarised requires-extent{b: 8} / {b: n*4} and checked at every call ('put7' requires 8 bytes behind 'small', which has 4 bytes), through wrappers and across units; a need under a condition a summary cannot spell (min(n, 16), if (n > 4) b[4]) is not exported.
    • WEAVEC_SIZED_BY(n) (pointer parameters: at least n elements behind the pointer, bytes for void *): checked inside the body and at every call; invalid-annotation on a non-pointer or naming no integer parameter. weavec.h 0.6.
    • lifetime-too-short is decided when the pointee dies rather than at the store: a store undone before then (ls->fs = fs.prev), or into a holder that is dead by then, is not reported. The L->fs = &fs; ... L->fs = fs.prev idiom that produced every Lua lifetime-too-short is clean.
    • The whole-program fixpoint (RFC 0005) widens a cyclic group after a fixed number of rounds (each member’s exports are joined with the previous round’s) so it converges on every input; the round cap is a safety net rather than the usual exit.
    • Summary text format version 6 → 7: @<offset> on effects and copies, extent= on fresh sources, and requires-extent lines; sidecar format version 7. --dump-analysis prints offsets on alias edges (q~p@+4), spatial{} (extents and offsets) and relations{} in states, and requires-extent{} in summaries and in the program database dump.
    • Recall check: test/recall/CWE-*/*.c are Juliet-style cases (a bad function with a // RECALL: <id> @<line> pin and good functions that must be clean) for CWE-121, 122, 124, 126, 127 (buffer overflows, underwrites and over-reads), 401 (leak), 415 (double free), 416 (use after free), 457 (uninitialised) and 476 (null dereference); scripts/recall.py runs them, prints recall per CWE and fails on any missed pin or any report in a good function. Wired into ctest (recall) and CI.
  • Spatial safety II (RFC 0012): strings, sized fields, offset relations and assumptions.

    • String facts: beside its extent an object carries the length of the string it holds (a constant, strlen(s) as a length place, or a variable equal to one) or the fact that it has no terminator, on the object and every exact alias of it. Sources: literals and initialisers; strcpy, stpcpy, strcat, sprintf, strdup, fgets, snprintf; 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 (no terminator); a NUL store; every other write forgets.
    • out-of-bounds for the string copies against the destination’s extent: 'strcpy' accesses 6 bytes of 'buf', which has 4 bytes, 'strcpy' accesses 'strlen(s)' + 1 bytes of 'd', which has 'strlen(s)' bytes (malloc(strlen(s)), also through n = strlen(s)), 'strcat' accesses 5 bytes of 'buf', which has 4 bytes (counting what buf holds), 'sprintf' accesses at least 5 bytes of 'buf', which has 4 bytes (the format’s minimum); and for terminator-seeking reads (strlen, strcpy’s and strcat’s source, puts, printf("%s")) of an object known to have none: 'strlen' reads past the end of 'name', which is not NUL-terminated, note 'name' is left without a terminator here. A copy that overflowed leaves the string unknown, so it is reported once. The _FORTIFY_SOURCE forms of the printf family (__builtin___sprintf_chk and friends, which put a flag and a size before the format) have their own library-table rows, so the checks see them too; on macOS this also means an unchecked malloc result passed to sprintf is a null-dereference there as it already was on Linux (snprintf’s forms keep accepting a null destination).
    • WEAVEC_SIZED_BY(g) on pointer fields (struct buf { char *WEAVEC_SIZED_BY(cap) data; size_t cap; }): every load of the field has cap elements of extent ('b->data[b->cap]' is out of bounds: 'b->cap' is the number of elements of 'b->data'), and a store of a smaller object is an annotation-mismatch ('b->data' is declared WEAVEC_SIZED_BY(cap) but is given 4 bytes where 'b->cap' says 8, at the store or at the count’s write, whichever is second). invalid-annotation on a non-pointer field or one naming no integer sibling, once per unit.
    • Inferred sized fields: every store into a pointer field of a named record is a witness (v->items = malloc(n * sizeof *v->items); v->cap = n;) or a refutation (a store of an object no sibling counts; a write to a count with no store into the pointer); a pair witnessed with one count and scale and refuted nowhere in the program is in force for every load. Within a unit the readers of a newly confirmed field are analysed once more and only their new reports shown; across units the whole-program driver does the same for units that looked the field up before the program confirmed it, and weavec-cc’s link step re-analyses an object whose sidecar says it did.
    • Offset relations and lower bounds: i <= n - 1 is i < n, j = i + 1 carries into a[j] ('a[i + 1]' may be out of bounds: 'i' may reach one below 'n', and 'a' has 'n' * 4 bytes), and a constant lower bound decides outright ('buf[i]' is out of bounds: 'i' is at least 8 in an object of 8 bytes).
    • WEAVEC_ASSUME(expr): expr holds from the call on, as on the true edge of if (expr); a contradicted assumption ends the path; weavec.assume on any other function is invalid-annotation. weavec.h 0.7.
    • Sidecar format version 8: sized-field <f> <g> <scale>, unsized-field <f> [<g>] and loads-field <f> lines (summary text format unchanged at 7). --dump-analysis prints string facts in spatial{} (s string=len(strlen(s))), i >= 8 in relations{}, and the program’s sized-field facts after count-field.
    • Recall: CWE-170 (improper null termination) joins the set; CWE-121, 122 and 126 gain the string shapes (strcpy of a literal, strcat, sprintf, malloc(strlen(s)), strdup indexed past its end, strlen of an unterminated array) and CWE-122 the sized-field ones.
  • Outcome classes keep their guards (RFC 0009, Guards). if (nsize == 0) { free(ptr); return NULL; } return realloc(ptr, nsize); (Lua’s l_alloc) is summarised outcome null{ptr: freed when nsize =0} outcome nonnull{ptr: moved} instead of an unconditional free; a caller that tests the result and knows the size is non-zero still owns the block on the failure path, and the classes and their guards survive wrappers (if (nb == NULL && nsize > 0), if (nv == NULL) { /* keep */ } else t->hash = nv;). Two narrowings of one call’s outcome that meet at a join are one outcome again rather than being forgotten.

  • Pass optional access starts directly through bounds checking and requirement propagation, avoiding unwrap-and-rewrap conversions rejected by clang-tidy.

  • Cache constant operands during modular range multiplication so clang-tidy checks the same optional values it later reads, avoiding a Linux CI uninitialized-value false positive. Retain coverage for both operand orders. Use explicit empty defaults for optional product types and append expression descriptions without temporary string concatenations to satisfy header checks.

  • A null test of a pointer made every exact alias of it definitely null, including aliases the relation only holds on some path (two pointers into the same object at the same field on one loop iteration): Lua’s if ((newci = luaD_precall(L, ra, n)) == NULL) updatetrap(ci); made ci null and every later ci-> a null-dereference. A null claim now travels only to a copy whose own record still agrees with the tested place’s; NonNull travels as before (RFC 0011, Deriving a pointer).

  • A returned local that aliased both a caller’s place (ci = L->ci) and the base of a derived pointer (L at +base_ci) could be summarised by the derived name; the exact alias is preferred (return copy L->ci).

  • Freeing an object reported a conflicting-borrow for a borrow of an object the freed one merely pointed at (*parents->buckets->last, a pair jansson’s intrusive list owns, when hashtable_do_rehash frees the bucket array). The check now looks only at loans on the released storage (the object and its fields, without crossing another dereference); what the object’s pointers own is released by a consume of its own, with its own check (RFC 0011, Deriving a pointer).

  • f = fs->f; f->upvalues = grow(...); return &f->upvalues[n] (Lua’s allocupvalue) was summarised as returning a fresh allocation, so every caller leaked the pointer it got back ('up' is leaked); it is a copy of the caller’s own fs->f->upvalues (RFC 0011, Deriving a pointer).

  • A void callee that frees what an argument points into only under a guard (moveresults: res: freed when[fwanted positive|negative]) had every copy of that argument read as a fresh block handed back; consumesUnconditionally now honours the effect’s own guard when there are no outcome classes (RFC 0009, Outcome classes).

  • An integer constant was read as its two’s-complement bits rather than its value, and every comparison as signed: ULONG_MAX was -1, so for index = 0 the edge on which if (index > ULONG_MAX) fails was infeasible and everything after it unchecked (a null-dereference in cJSON’s create_patches went unreported). A constant is now its mathematical value in its own type (unsigned x = -1 is UINT_MAX; SIZE_MAX is no constant the checker holds and decides nothing), an unsigned comparison is decided in unsigned order (a negative signed operand converted up ranks above every non-negative value) and a case label is converted to the scrutinee’s type (RFC 0009, Assumptions).

  • A callee that released a value the caller had already released and left a new one in its place (replaced, RFC 0008) was reported once and then again at every later call, because the stale record survived when no store named the place in the caller’s terms (the callee reached it through an alias of its own). The place now holds the new value after the one report.

  • A callee whose only effect below a pointer argument was a consume (free(L->stack)) was replayed into its caller’s summary as having overwritten the whole object (*L: written), which made the caller’s callers forget everything below L, including that L->stack was gone. Only a summary with no effect at all below the pointee is that coarse (RFC 0006, written forgets what lies below).

  • free(static_array) and free(local_array) crashed the checker (getPointeeType on an array declaration in checkContainerFree); they are now invalid-release reports (RFC 0008).

  • The whole-program fixpoint (RFC 0005) rebuilt its database by renumbering every member’s summaries each time one member’s exports changed, which on Lua (34 units in one cycle) was most of the run once RFC 0008 made the summaries larger. Members are now kept numbered by the database’s own table (ProgramDatabase::renumbered, GlobalNames::extendTo) and a rebuild copies them.

  • BorrowState kept one loan per site of a borrow, so a callee’s store applied at a hundred call sites was a hundred loans copied at every block visit and merged at every join (1,173 per state in Lua’s luaV_execute). It keeps one per borrow at the earliest site, which is the one a conflict cited anyway (BorrowState::sameBorrow).

  • Applying a callee’s summary consumed shallower paths before deeper ones, so static void both(struct box *b) { free(b->p); free(b); } followed by a use of a caller’s copy of b->p was not reported: freeing b first dropped the facts under it before b->p’s consumption reached the alias. Consumed paths are now applied deepest first; memory below an object the same call frees is consumed on its own only when the caller knows the place, and reported once (at the object) when the object is already gone (RFC 0007, Applying a summary: deepest paths first).

  • putenv keeps its string and setvbuf keeps its buffer in the shipped table (RFC 0007, Assumptions).

  • a->f on an array (printbuffer buffer[1]; buffer->buffer = ...) is the place a[0].f, as *a already was a[0]; it used to be the element summary a[*].f, whose null store could not clear a record.

  • Condition facts on the right operand of || / &&: the block that evaluates (p = malloc(n)) == NULL in if (fd == -1 || (p = malloc(n)) == NULL) return NULL; branches on that operand, but Clang hands back the whole condition; the null edge did not clear p’s record and the return was a false leak.

  • Freeing memory reached below a borrowed object is not a conflicting-borrow: z_streamp strm = &state->strm; inflateInit2(&state->strm, ...), whose callee frees state->strm.state->window, left strm pointing at storage nothing released. Loans on ancestors of the consumed place no longer count for the consume query (RFC 0006, Conflict rules, amended).

  • A leak at the end of an address-taken local’s scope is reported on the statement the scope ends after (the return), not on the declaration.

  • A block ending in a noreturn call no longer flows into the function’s exit state, so what such a path frees (Lua’s os_exit closing the state behind exit) does not become a freed effect of the summary and a double-free at every caller; the summary describes the state after a return (RFC 0007, Interaction with existing RFCs).

  • On the null edge of a pointer test every fact below the pointer is dropped (there is nothing there), so records, moves and aliases of the pointer’s fields no longer report on a path where the pointer is null.

  • A whole write to a field also clears the move records of the same cell under the pointer’s aliases (free(L->stack); L->stack = fresh with L->twups ~ L left L->twups->stack freed for good), which on Lua made every second luaD_reallocstack a double-free (RFC 0002, Alias relation, implementation notes).

  • An &&/|| under !, __builtin_expect or != 0 is computed as a value before the branch, so only the whole value is known on an edge: a true && or a false || now holds each operand (Lua’s l_unlikely(newblock == NULL && nsize > 0) makes newblock null, and overwriting it is no leak), and the other edges say nothing, where the right operand alone used to be taken (if (__builtin_expect(n > 0 && p != NULL, 1)) { free(p); return 0; } return -1; was wrongly clean).

  • Two paths of one callee summary that name the same cell through the caller’s aliases (g->allgc and g->twups->l_G->allgc with g->twups ~ L, Lua’s luaC_freeallobjects) are one release, not a double-free (RFC 0007, Applying a summary: deepest paths first).

  • A value stored below a local that borrows caller memory or a global (tb = &G(L)->strt; tb->hash = newvect, Lua’s luaS_resize) escapes: the store landed in an object that outlives the function under a name the summary cannot report, and the last local name’s death was a false leak (RFC 0007, Escape).

  • The corpus baseline (scripts/corpus/baseline.json) is refreshed for RFC 0011: conflicting-borrow 16 → 2, lifetime-too-short 18 → 4, null-dereference 189 → 171, leak 20 → 17, invalid-release 6 → 5, double-free 81 → 82, use-after-free 439 → 663 (the last two Lua’s luaV_execute family, larger now that ci->func.p and ci->top.p are named as pointers into the stack), out-of-bounds 0; whole corpus 105 s (Lua from 3 min 22 s to 1 min 46 s). The per-project triage is in scripts/corpus/README.md.

  • Dereferencing an allocator’s result without testing it (p = malloc(n); p->x = 1;) is now a null-dereference error (RFC 0008). The existing unit-test and lit snippets that did this gained an if (!p) return;; the inferred summaries of functions that return or store an untested allocation gained null among their returns / stores, and functions that dereference a parameter gained requires{...}.

  • The RFC 0007 leak check found real leaks in the existing unit-test snippets (realloc success paths, an OWNED parameter that was only looked at, a switch without default, a loop whose free is behind break); their expectations now include the leak.

  • A callee’s summary store into a place that holds a resource this function made owned escapes the old value instead of reporting an overwrite: RFC 0003 shows the caller only the store for the far more common free(b->data); b->data = NULL; (RFC 0007, Deliberately not caught).

  • A call with a mutably borrowed argument copies the callee’s written paths below the argument into the caller’s summary (L->nci: written, L->ci->top.p: written, …) instead of marking the pointee itself written, which told every caller the whole object had been overwritten and made it forget everything it knew below the argument (Lua’s close_state lost the frees freestack reported to it). Summaries on Lua-sized programs are an order of magnitude longer as a result; the paths are resolved incrementally, cached per call while no new place is interned, and copied once per call and pointee, but the Lua program still takes about twice as long as before (RFC 0006, What a callee wrote, its caller wrote; RFC 0007, Performance). The three new Lua conflicting-borrow reports are facts this used to erase (close_state frees L->l_G while L, an interior pointer into it, is live), of the interior-pointer kind RFC 0001 already accepts.

  • A callee that consumes a path below an argument or a global and returns a copy of it (t->array = resizearray(L, t, ...)) makes the result the same resource, now owned by the result, as RFC 0003 already did for consumed parameters (RFC 0006, Interaction with existing RFCs). Only when the path is moved or consumed on every class: a copy of a path freed on some classes only (zlib’s gz_look copying state->out, which gz_fetch frees on its error class) is not tracked, otherwise the copy’s later overwrite was a false leak (RFC 0007, Applying a summary: deepest paths first).

  • (res = feed()) == sentinel and (p = f()) != q are pointer-equality condition facts about res / p (RFC 0006), so the “loop until the reader returns something other than the sentinel” idiom is clean.

  • Analysis time on large functions and programs. A dead local’s alias edges are dropped with its loans (RFC 0006, Performance); AnalysisState::join reports whether it changed instead of the engine copying and comparing states; PlaceTable::descendants walks the subtree instead of the table; BorrowState keeps its loans sorted; loan expiry runs only where a variable dies; the whole-program database is rebuilt only after a unit’s exports changed. Lua’s lvm.c went from 56 s to 3 s and the Lua program from 23 minutes to under 6. No diagnostic changed.

  • conflicting-borrow no longer rejects two live borrows of one object or a write to a borrowed object by default (RFC 0006, Conflict rules): int *a = &x; int *b = &x;, char *p = buf; snprintf(buf, ...); use(p); and int *pa = &s->a; s->a = 2; use(pa); are accepted. Freeing or moving a borrowed object is still reported. --exclusive-borrows restores the RFC 0001 rule with the messages unchanged.

  • free(a[0]); use(a[1]); and the loop-free idiom are no longer reported (RFC 0006, Element witnesses); free(a[i]); use(a[i]); still is.

  • if (free_if(p, c)) return; p[0] = 1; is clean when free_if frees only on the paths returning non-zero (RFC 0006); untested, the may-free is still reported.

  • ValueSource::copy from strchr-like table entries is now interiorCopy; Store values for strto* end pointers and strtok_r’s save pointer likewise.

  • SummaryFormatVersion 1 → 2 and SidecarFormatVersion 1 → 2: version-1 sidecars are rejected by their header and the objects re-analysed.

  • MoveTracker::markMoved/movedAt/reinitialize take an ElementWitness; AliasRelation::unite takes exactness and witnesses; FunctionSummary::reallocLike and CallEffects::isRealloc are removed; AnalysisState::reallocs is replaced by pending.

  • A whole-struct assignment or initialisation (b = a, struct buf b = a;, *p = s) copies the facts of every pointer-typed field (aliases, loans, moves, raw records, kinds) instead of forgetting them (RFC 0005), so b = a; free(a.data); b.data[0] is a use-after-free. Fields with no place under the source are still forgotten.

  • annotation-required fires for a callee with no definition anywhere in the program (previously: in the translation unit), once per callee per program; in weavec-cc it is deferred from the compile step to the link step. The second note now ends or define it in this program; the indirect form says in this program instead of in this translation unit.

  • --dump-analysis in whole-program mode prefixes each unit’s dump with unit '<source>':.

  • tools/weavec accepts zero source files with -p (every file of the database is analysed).

  • SccFinder moved from TranslationUnitAnalysis.cpp to core::stronglyConnectedComponents (Core/Scc.h).

  • cmake/WeaveCLLVM.cmake records WEAVEC_CLANG_EXECUTABLE; frontend::getClangExecutable().

  • WEAVEC_UNSAFE blocks and function bodies are analysed instead of skipped (RFC 0004): diagnostics inside the region are suppressed, raw operations are permitted, but ownership effects flow out of it, so WEAVEC_UNSAFE { free(p); } p[0] is now a use-after-free at p[0] and a WEAVEC_UNSAFE function’s callers see its inferred effects. A WEAVEC_UNSAFE declaration without a body is unchanged (empty summary, no boundary warning).

  • Pointer arithmetic (p + 1, p++, &a[i]) and casts between pointer types preserve the identity of the pointed-to object instead of producing an untracked value (RFC 0004), so q = p + 1; free(p); q[0] is a use-after-free and bind(fd, (struct sockaddr *)&addr, len) borrows addr. Only integer-to-pointer casts lose identity, and they yield a raw pointer.

  • --strict-externs (RFC 0004): a call the checker cannot resolve is now an unsafe-operation error at every call site outside a WEAVEC_UNSAFE region (system headers included) and its pointer result is raw, instead of an annotation-required error once per callee. Inside an unsafe region it is silent.

  • annotation-required’s notes mention WEAVEC_RAW; a new form covers calls through function pointers with no signature.

  • analysis::AnnotationSet::safeKind() returns std::optional<core::OwnershipKind>; AnnotationSet gained raw, ownership() and merge(); analysis::ValueOrigin gained Raw and rawReason.

  • double-free and use-after-free are now also reported for the second iteration of a loop that frees a pointer declared outside it.

  • AnalysisOptions gained dumpStream; core::Loan gained holder and core::MoveRecord gained via.

  • Copying a pointer that holds a loan into a longer-lived pointer (g = p where p = &local) is now lifetime-too-short, like g = &local already was.

  • Calls to unannotated functions now borrow their pointer arguments for the duration of the call (previously: no effect), so set(&x) while x is borrowed is a conflicting-borrow.

  • --report-unannotated no longer reports static functions or main, and its message names the inferred annotation.

  • analysis::CallEffects is now backed by a core::FunctionSummary (releasesArgs replaced by frees(i); classifyCall takes a SummaryStore).

  • LocalOwnershipChecker (superseded by FunctionDataflow).