diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0804de2..3049946 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -77,6 +77,9 @@ jobs: - name: Linux / Clang / Debug + ASan/UBSan os: ubuntu-24.04 preset: ci-debug + # RFC 0030 (gate H1): the test/cases suites build, diagnose and + # write ledgers under ASan, without running the case programs. + configure-args: -DWEAVEC_CASES_ARGS=--no-run - name: Linux / Clang / Release os: ubuntu-24.04 preset: ci-release @@ -125,41 +128,55 @@ jobs: max-size: ${{ env.CCACHE_MAXSIZE }} - name: Configure - run: cmake --preset "${{ matrix.preset }}" + run: cmake --preset "${{ matrix.preset }}" ${{ matrix.configure-args }} - name: Build run: cmake --build --preset "${{ matrix.preset }}" + # Unit, lit and the test/cases suites (one cases- test per + # directory of test/cases, RFC 0030 section 17.4), in parallel. - name: Test env: ASAN_OPTIONS: detect_leaks=0:strict_string_checks=1 UBSAN_OPTIONS: print_stacktrace=1:halt_on_error=1 - run: ctest --preset "${{ matrix.preset }}" + run: ctest --preset "${{ matrix.preset }}" -j "$(getconf _NPROCESSORS_ONLN)" - name: Documentation examples - run: python3 docs/scripts/check-examples.py --weavec "build/${{ matrix.preset }}/bin/weavec" + env: + ASAN_OPTIONS: detect_leaks=0 + run: | + python3 docs/scripts/check-examples.py \ + --weavec "build/${{ matrix.preset }}/bin/weavec" \ + --weavec-cc "build/${{ matrix.preset }}/bin/weavec-cc" - # ctest already ran the recall set; run it once more here so the - # per-CWE table is in the log (RFC 0011, *Recall check*). - - name: Recall - run: python3 scripts/recall.py --weavec "build/${{ matrix.preset }}/bin/weavec" + # RFC 0030 gate H2: no checked-mode residue, no library names compared + # outside the LibrarySpec table, no corpus project names in lib/, the + # engine seam, and the Dataflow and library line budgets. + - name: Repository hygiene + if: runner.os == 'Linux' && matrix.preset == 'ci-release' + run: | + python3 scripts/test_check_hygiene.py + python3 scripts/check-hygiene.py - # RFC 0014: fixed source revisions exercise real callback-heavy code. - # Counts are retained for review; parse errors, crashes, timeouts and - # nonconvergence fail the gate on both release platforms. + # RFC 0030 (section 17.5): per-file compiles and whole-program analyses of + # the pinned corpus configurations in test/corpus/, checked against the + # ratchet in test/corpus/expected.json and the triage in + # test/corpus/triage.json. The weekly Corpus workflow runs --full. - name: Pinned corpus if: matrix.preset == 'ci-release' run: | - python3 scripts/corpus.py --weavec "build/${{ matrix.preset }}/bin/weavec" \ - --manifest scripts/corpus/rfc0014.json --timeout 120 \ - --measure-memory --json corpus-rfc0014.json + python3 scripts/corpus-gate.py --quick \ + --weavec "build/${{ matrix.preset }}/bin/weavec" \ + --weavec-cc "build/${{ matrix.preset }}/bin/weavec-cc" \ + --only log.c --only cJSON-program --only linenoise-program \ + --only jansson --json corpus-gate-quick.json - name: Upload pinned corpus results if: always() && matrix.preset == 'ci-release' uses: actions/upload-artifact@v7 with: - name: corpus-rfc0014-${{ matrix.os }} - path: corpus-rfc0014.json + name: corpus-gate-quick-${{ matrix.os }} + path: corpus-gate-quick.json if-no-files-found: ignore - name: Smoke-test install @@ -181,6 +198,7 @@ jobs: path: | build/${{ matrix.preset }}/Testing/Temporary/LastTest.log build/${{ matrix.preset }}/test/**/Output/** + build/${{ matrix.preset }}/test/cases/cases-*.json if-no-files-found: ignore # --------------------------------------------------------------------------- diff --git a/.github/workflows/corpus.yml b/.github/workflows/corpus.yml index 1f9e9db..db4d63d 100644 --- a/.github/workflows/corpus.yml +++ b/.github/workflows/corpus.yml @@ -1,8 +1,10 @@ name: Corpus -# Runs weavec over the real-world projects in scripts/corpus/projects.json -# and compares diagnostic counts with scripts/corpus/baseline.json. Not part of -# the PR gate: the projects track branches and can change under us. +# Runs the full corpus gate (RFC 0030, section 17.5) over the projects pinned +# by SHA in test/corpus/manifest.json: per-file compiles, whole-program +# analyses, project builds, test suites, injections and benchmarks, checked +# against test/corpus/expected.json and test/corpus/triage.json. The gate +# clones the projects into build/corpus. Pull requests run --quick in CI. on: schedule: - cron: "17 6 * * 1" @@ -18,7 +20,9 @@ jobs: corpus: name: Corpus regression runs-on: ubuntu-24.04 - timeout-minutes: 45 + # --full builds and tests every project, applies each injection and runs + # the benchmarks, so it needs more time than the analysis-only run did. + timeout-minutes: 120 steps: - uses: actions/checkout@v7 @@ -49,15 +53,17 @@ jobs: cmake --preset ci-release -DWEAVEC_BUILD_TESTS=OFF cmake --build --preset ci-release - - name: Run corpus + - name: Run corpus gate run: | - scripts/corpus.py --weavec build/ci-release/bin/weavec \ - --json corpus-results.json \ - --baseline scripts/corpus/baseline.json + python3 scripts/corpus-gate.py --full \ + --weavec build/ci-release/bin/weavec \ + --weavec-cc build/ci-release/bin/weavec-cc \ + --json corpus-gate-full.json - name: Upload results if: always() uses: actions/upload-artifact@v7 with: - name: corpus-results - path: corpus-results.json + name: corpus-gate-full + path: corpus-gate-full.json + if-no-files-found: ignore diff --git a/AGENTS.md b/AGENTS.md index eef92b8..6901687 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -5,28 +5,40 @@ most and where to find the rest. ## Project in one paragraph -WeaveC is a Clang/LLVM-based tool that adds inferred ownership and borrowing -checks to C. Three C++ libraries: `weavec::Core` (the ownership model, **no -Clang/LLVM includes allowed**), `weavec::Analysis` (Clang AST → core facts; -the only layer that includes both), `weavec::Frontend` (Clang -`FrontendAction`, whole-program orchestration, sidecars, the compiler -driver, diagnostics bridging). `tools/weavec` is a libTooling CLI; -`tools/weavec-cc` is a drop-in C compiler (Clang's driver with WeaveC -inside) that analyses the whole program at link time (RFC 0005). -Full picture: `docs/architecture.md`; model semantics and the reasoning -behind them: `docs/rfcs/` (start with `0001-ownership-model.md`). +WeaveC is a Clang/LLVM-based C compiler and analysis tool that adds inferred +ownership and borrowing to C. For every safety facet (spatial, null, +temporal) of every memory operation it records one outcome in a *ledger*: +proven, checked by a runtime check it inserts, a definite violation (an +error), or unresolved or trusted with a reason. Three C++ libraries: +`weavec::Core` (the model, the ledger, pointer kinds, the library table; +**no Clang/LLVM includes allowed**), `weavec::Analysis` (Clang AST → core +facts: sites, kinds, the engine behind the `SafetyEngine` seam, the check +planner; the only layer that includes both), `weavec::Frontend` (deferred +CodeGen, check emission, zero-initialisation, ledger writers, unit records, +whole-program orchestration, the compiler driver, diagnostics bridging). +`runtime/` holds the small C runtime for report mode and precompiled +headers. `tools/weavec` is a libTooling CLI; `tools/weavec-cc` is a drop-in C +compiler (Clang's driver with WeaveC inside) that inserts the checks and +analyses the whole program at link time. Full picture: +`docs/architecture.md`. Model semantics and the reasoning behind them: +`docs/rfcs/`. Read `0001-ownership-model.md` first, then +`0030-prove-or-trap.md`, which is the current model: it replaces RFC 0001's +guarantee, amends RFCs 0002–0017 where they say so, and supersedes RFCs +0018–0029. There is no checked mode. ## Before touching the model or the checker -Design decisions for `Core`, `lib/Analysis/Dataflow.cpp` (the checker), -`weavec.h`, diagnostic ids, and what crosses translation units (exports, -the program database, the sidecar) are recorded as RFCs in -`docs/rfcs/`. **Read the relevant RFC before changing any of these**, and -treat it as authoritative over comments in the code. If the change you are -about to make is not covered by an Accepted RFC, or contradicts one, stop and -write or amend an RFC first (`docs/rfcs/README.md` explains when one is -required and the process); do not encode a new design decision in code -alone. Bug fixes that bring code in line with an RFC need no RFC. +Design decisions for `Core`, the checker (the engine behind `SafetyEngine`, +today `FunctionDataflow` in `lib/Analysis/Dataflow*.cpp`), the ledger and +its outcomes and reasons, `LibrarySpec.txt`, `weavec.h`, diagnostic ids, +the inserted checks, and what crosses translation units (exports, the +program database, the unit record) are recorded as RFCs in `docs/rfcs/`. +**Read the relevant RFC before changing any of these**, and treat it as +authoritative over comments in the code. If the change you are about to +make is not covered by an Accepted RFC, or contradicts one, stop and write +or amend an RFC first (`docs/rfcs/README.md` explains when one is required +and the process); do not encode a new design decision in code alone. Bug +fixes that bring code in line with an RFC need no RFC. ## Build and test @@ -38,6 +50,10 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev - Unit tests: `build/dev/unittests/WeaveC{Core,Analysis,Frontend}Tests`. - Integration tests: `lit -v build/dev/test` (FileCheck-based; see `test/README.md`). +- Test cases: `scripts/run-cases.py [--filter 'soundness/**']` (see + `test/cases/README.md`); CTest runs them as `cases-`. +- Corpus gate: `scripts/corpus-gate.py --quick` (see `test/corpus/README.md`). +- Hygiene gate: `scripts/check-hygiene.py`. - Format: `scripts/format.sh`; check: `scripts/check-format.sh`. ## Rules that reviewers will enforce @@ -45,8 +61,9 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev 1. Never add `clang/` or `llvm/` includes under `include/weavec/Core` or `lib/Core`. 2. Every new diagnostic gets a stable id in `weavec::core::diag` - (`include/weavec/Core/Diagnostic.h`), an entry in `docs/annotations.md`, - a unit test, and a lit test that pins the exact message. + (`include/weavec/Core/Diagnostic.h`), an entry in `docs/annotations.md` + and `docs/data/diagnostic-remedies.json`, a unit test, and a lit test that + pins the exact message. 3. Annotation spellings live in exactly two places that must agree: `include/weavec/Analysis/Annotations.h` (`spelling::`) and `resources/include/weavec.h`. @@ -57,31 +74,48 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev than anonymous namespaces); `.clang-tidy` enforces it. 6. Use Conventional Commit PR titles and document user-visible changes in the relevant guides. `CHANGELOG.md` is generated solely by semantic-release; - do not edit it manually. Pre-0.1.0 notes are archived in - `docs/development-history.md`. + do not edit it manually. 7. Do not commit generated files (`build/`, `compile_commands.json`). 8. Changes to `Core`, checker rules, annotations or diagnostic ids reference - the RFC that specifies them (in the PR and, for lit tests, in the - filename: `test/Analysis/rfc0002-*.c`). + the RFC that specifies them in the PR. New tests are named by feature + (`test/cases//…`, `test/Emission/-*.c`); existing + `rfcNNNN-` names may stay. +9. Keep the engine seam and the library table clean (gate H2, + `scripts/check-hygiene.py`): only `DataflowEngine.cpp`, + `FunctionAnalysis.cpp`, `CallbackSummaries.cpp`, + `CallContextSummaries.cpp`, `KindSeeding.cpp` and the `Dataflow*.cpp` + files include `Dataflow.h`; `FunctionDataflow` publishes only through `LedgerAdapter` + and never receives a `DiagnosticSink`; library behaviour goes in + `lib/Core/LibrarySpec.txt`, never in `name == "…"` tests; nothing under + `lib/` names a corpus project; library code stays within its line + budget. ## Where things are | Task | Look at | | ------------------------------------ | ------------------------------------------------------ | | Propose a model / checker change | `docs/rfcs/README.md`, `docs/rfcs/0000-template.md` | -| Add a checker rule | `lib/Analysis/Dataflow.cpp` (after an RFC) | +| Add a checker rule | After an RFC, behind the seam: the engine (`lib/Analysis/Dataflow*.cpp`, run by `DataflowEngine`) publishes only through `LedgerAdapter` (`include/weavec/Analysis/LedgerAdapter.h`, `SafetyEngine.h`) | +| Change outcomes, reasons, the summary line | `lib/Core/Ledger.cpp`, `lib/Analysis/LedgerAdapter.cpp` (defaults, rollup) | +| Change which sites exist | `lib/Analysis/SiteCollector.cpp` | +| Change pointer kinds / how annotations become kinds | `lib/Core/PointerKind.cpp`, `lib/Analysis/AttributeReader.cpp`, `lib/Analysis/KindInference*.cpp`; what the engine takes from them: `lib/Analysis/KindSeeding.cpp` | +| Change which checks are inserted | `lib/Analysis/CheckPlanner.cpp` (plan), `lib/Frontend/CheckEmitter.cpp` and `Prelude.cpp` (emission), `runtime/` | +| Change zero-initialisation | `lib/Frontend/ZeroInit.cpp` | | Map an expression to a place | `lib/Analysis/PlaceBuilder.cpp` | -| Recognise an allocator / releaser | `lib/Analysis/Allocators.cpp`, `lib/Analysis/Builtins.cpp` (libc table) | +| Model a C library function / allocator / releaser | `lib/Core/LibrarySpec.txt` (one unit test per row in `unittests/Core/LibrarySpecTest.cpp`), `lib/Analysis/Allocators.cpp` | +| Change function-pointer slots | `lib/Core/FnSlots.cpp`, `lib/Analysis/SlotCollector.cpp` | | Change how a callee's summary is found | `lib/Analysis/Summaries.cpp` (`SummaryStore`, RFC 0003/0005) | -| Change the TU driver / call graph | `lib/Analysis/TranslationUnitAnalysis.cpp` | +| Change the TU driver / call graph | `lib/Analysis/TranslationUnitAnalysis.cpp`, `lib/Analysis/UnitPipeline.cpp` | | Change what a unit exports / the program database | `lib/Analysis/ProgramDatabase.cpp` (RFC 0005) | | Change the summary text format | `lib/Core/SummaryIO.cpp` (versioned; round-trip tests) | -| Change the whole-program algorithm | `lib/Frontend/ProgramAnalysis.cpp` | -| Change the sidecar file (`foo.o.weavec`) | `lib/Frontend/Sidecar.cpp` (bump `SidecarFormatVersion`) | +| Change the whole-program algorithm / link step | `lib/Frontend/ProgramAnalysis.cpp`, `lib/Frontend/Driver.cpp` | +| Change the unit record (`foo.o.weavec`) | `lib/Frontend/UnitRecord.cpp` (format 28; the schema fingerprint follows the codec's field table), `lib/Frontend/Sidecar.cpp` | +| Change the ledger JSON / SARIF | `lib/Frontend/LedgerWriter.cpp`, `lib/Frontend/LedgerOutput.cpp` | | Change `weavec-cc` (driver, cc1 wrapping, link step) | `lib/Frontend/Driver.cpp`, `tools/weavec-cc/main.cpp` | | Change `-W` / `-fweavec-*` handling | `lib/Frontend/DiagnosticControl.cpp`, `DriverOptions` in `Driver.h` | -| Debug what the checker inferred | `weavec --dump-analysis file.c --`; `weavec --whole-program --dump-analysis a.c b.c --` | -| Measure precision on real code | `scripts/corpus.py`, `scripts/corpus/README.md` | +| Debug what the checker inferred | `weavec --dump-analysis file.c --`; `weavec --dump-kinds file.c --`; `weavec --ledger=out.json file.c --`; `weavec --whole-program --dump-analysis a.c b.c --` | +| Add or run a test case | `test/cases/README.md`, `scripts/run-cases.py` | +| Measure precision on real code | `scripts/corpus-gate.py`, `test/corpus/` (README, manifest, expected ratchet, triage) | | Change how diagnostics are rendered | `lib/Frontend/ClangDiagnosticSink.cpp` | | Add a CLI flag | `tools/weavec/main.cpp`, `FrontendOptions`; driver flags in `Driver.h` | | Add an annotation | `Annotations.h`, `weavec.h`, `docs/annotations.md` | diff --git a/CMakeLists.txt b/CMakeLists.txt index e59ea49..8968c1b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -104,6 +104,9 @@ add_subdirectory(lib) if(WEAVEC_BUILD_TOOLS) add_subdirectory(tools) + # RFC 0030: libweavec_rt.a and libweavec_chk.a (the latter generated with + # `weavec-cc -fweavec-print-prelude=out-of-line`). + add_subdirectory(runtime) endif() if(WEAVEC_BUILD_TESTS) diff --git a/CMakePresets.json b/CMakePresets.json index 00dc388..0c725e1 100644 --- a/CMakePresets.json +++ b/CMakePresets.json @@ -121,6 +121,7 @@ { "name": "test-base", "hidden": true, + "environment": { "CTEST_PARALLEL_LEVEL": "" }, "output": { "outputOnFailure": true }, "execution": { "noTestsAction": "error", "stopOnFailure": false } }, diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9b3f900..bfd5cc1 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -93,11 +93,13 @@ Additional rules: - **Warnings** are errors in CI. Do not suppress warnings without a comment explaining why. - **Tests.** New checker behaviour needs both a unit test (in `unittests/`) - exercising the core logic and a lit test (in `test/`) exercising the - end-to-end diagnostic. Lit tests that pin behaviour specified by an RFC - carry its number in the filename (`test/Analysis/rfc0002-*.c`). - False-positive fixes need a regression test in `test/Analysis/clean.c` or a - new file. + exercising the core logic and an end-to-end test: a lit test (in `test/`) + when the exact diagnostic text matters, or a case under `test/cases/` + whose markers pin what must be reported, checked or left unproven (see + `test/cases/README.md`). New tests are named by feature + (`test/cases//…`, `test/Emission/-*.c`), not by RFC number; + existing `rfcNNNN-` names may stay. False-positive fixes need a regression + case under `test/cases/` (a `// CLEAN` file). ## Commit messages @@ -121,8 +123,7 @@ and `chore` normally do not trigger a release. Optional scopes include `core`, Python Semantic Release generates `CHANGELOG.md` from the commit history; do not edit it manually. Document behavior and migration guidance in the -relevant guides and commit/PR descriptions. The earlier hand-written notes -are preserved in [the development history](docs/development-history.md). +relevant guides and commit/PR descriptions. ## Reporting bugs diff --git a/README.md b/README.md index b478db4..44190c8 100644 --- a/README.md +++ b/README.md @@ -5,210 +5,14 @@ [![CI](https://github.com/weavefoundry/weavec/actions/workflows/ci.yml/badge.svg)](https://github.com/weavefoundry/weavec/actions/workflows/ci.yml) [![License](https://img.shields.io/badge/license-Apache--2.0%20WITH%20LLVM--exception-blue.svg)](LICENSE) -A mostly source-compatible C compiler that brings Rust-style memory safety to existing C code through inferred ownership and borrowing. It automatically proves memory safety where possible, requires lightweight annotations only when necessary, and isolates truly unsafe operations behind explicit `unsafe` boundaries. The goal is to let teams incrementally make large C codebases memory-safe without rewriting them in Rust or abandoning the C ecosystem. - -WeaveC is built on Clang/LLVM rather than implementing a compiler from scratch, using Clang for parsing, semantic analysis, diagnostics, optimization, code generation, and platform support. WeaveC adds its own ownership inference, borrow checking, lifetime analysis, and memory-safety rules on top, allowing the project to focus on its core innovation while remaining compatible with the existing C toolchain and ecosystem. - -WeaveC itself is written in modern C++, which provides the most direct and complete access to Clang/LLVM's APIs and infrastructure. The core ownership, borrowing, lifetime, and inference logic should be kept as modular as possible so it remains cleanly separated from the Clang integration layer and can potentially be reused or extended in the future. - -> **Checked code:** RFCs 0018–0019 add opt-in, compositional safety checking with -> `--checked`, `--checked-function=name`, and `WEAVEC_CHECKED`. Selected -> functions must establish bounds, validity and initialization, or state their -> entry requirements and trusted boundaries. Unresolved operations fail the -> check even when warnings are disabled. This is a conditional guarantee for -> selected source functions within the supported model. Checked memory facts -> compose through nested buffers, constructors, output parameters, complete -> fill/copy loops, and modeled string and allocation operations. See -> [checked code](docs/checked-code.md) for scope, reports and compiler use. - -> **Status:** early. Function bodies are analyzed by a bounded dataflow ([RFC 0002](docs/rfcs/0002-intraprocedural-checking.md)): use-after-free and double-free through any alias and across loops, use-after-move, conflicting borrows, and pointers that outlive what they point to. Calls are modelled by inferred signatures ([RFC 0003](docs/rfcs/0003-signature-inference.md)): every function in the translation unit gets a summary of what it frees, writes, stores and returns, so `node_free(n); n->v` is caught without annotations; the C standard library and POSIX are covered by a shipped table, and annotations are checked against the bodies that carry them. Unsafe code has a boundary ([RFC 0004](docs/rfcs/0004-unsafe-boundaries.md)): pointers cast from integers or declared `WEAVEC_RAW` are *raw* and may only be dereferenced or released inside a `WEAVEC_UNSAFE` region, which is analysed rather than skipped; calls through function pointers are checked from the pointer type's annotations or from the functions assigned to it. Programs are analysed whole ([RFC 0005](docs/rfcs/0005-whole-program-analysis.md)): every translation unit exports the summaries of what it defines, so `other_free(o); o->v` is caught when `other_free` lives in another file, callbacks registered in one file are checked in the file that calls them, and unresolved direct or indirect calls are reported as boundaries. `weavec-cc` is a drop-in `cc` that does this as part of a normal build. The checker is precise where C idioms need it ([RFC 0006](docs/rfcs/0006-precision.md)): a borrow ends at the pointer's last use, not at the end of its scope; `if (p == sentinel) return; free(p);` knows the two are distinct; proven distinct array elements retain independent release history; and a function that frees its argument only when it returns `0` (or `NULL`) is summarised per outcome, so `if (rc != 0) free(p);` is clean while `if (rc == 0) use(p);` is reported. The other half of the ownership contract is checked too ([RFC 0007](docs/rfcs/0007-resource-lifecycle.md)): a resource that is never released is a `leak`, reported where it is lost (`if (c) return -1;` after a `malloc`, an overwrite, a discarded `strdup`, a `free(b)` that drops an owned `b->data`), and releasing it with the wrong function (`free` on a `FILE *`, through any wrapper, across files) is a `mismatched-release`. Pointers are checked for validity, not only ownership ([RFC 0008](docs/rfcs/0008-pointer-validity.md)): dereferencing a `malloc` result, a `strchr` result or any other pointer that may be null without testing it is a `null-dereference` (through calls too: a function that dereferences its parameter requires callers to prove it non-null), a pointer used before it is assigned is a `use-of-uninitialized`, `free` of a stack object, a string literal or the middle of an allocation is an `invalid-release`, and a callee that frees a value and then reinitialises the place (`realloc` in place, `free` then `= NULL`) still kills every copy of the old value the caller kept. The checker also knows *why* ([RFC 0009](docs/rfcs/0009-value-conditional-behaviour.md)): it tracks what is known about integers, so `if (c) free(p); ... if (!c) use(p);` and `switch (op) { case FREE: free(p); }` followed by another `switch` on `op` are clean; a callee's behaviour is summarised *per argument* (`l_alloc(ud, p, n, 0)` frees `p` and returns null, `l_alloc(ud, p, n, 64)` does not; `if (!b->noalloc) free(b->data)` frees only for callers that did not set the flag); and a function whose every path ends in `abort`, `exit`, `longjmp` or another such function is inferred `noreturn`, so `if (bad) die(); use(p);` is checked on the good path only. Objects with more than one owner are understood ([RFC 0010](docs/rfcs/0010-shared-ownership.md)): a reference count is inferred from the `obj_ref`/`obj_unref` pair that keeps it (`o->rc++`; `if (--o->rc == 0) free(o)`, in any spelling from `o->rc--` to `__atomic_fetch_sub`), so `b = obj_ref(a); obj_unref(b); use(a)` is clean while one `obj_unref` too many is a `double-free`, a use after the last one is a `use-after-free`, and a reference taken and dropped is a `leak`; a callee that stores its argument only on success (`if (bag_put(b, s) < 0) free(s);`) is summarised per outcome, and one that keeps its argument in a node of its own (`table_set(t, o)`) is known to have kept it. Memory is checked spatially as well as temporally ([RFC 0011](docs/rfcs/0011-spatial-safety.md)): a pointer is an object and an offset into it, so `free(container_of(i, struct outer, in))` frees what `i` belongs to and a field pointer kept across `free(p)` is a `use-after-free`; objects have a size (`malloc(n)`, `char buf[8]`, a wrapper's `xmalloc(n)`, a `WEAVEC_SIZED_BY(len)` parameter) and every subscript, dereference and `memcpy`/`memset`/`fgets`/`read` length is checked against it, through what the path knows of the index (`i <= n` on `malloc(n)` may reach one past the end; `i < 8` on four bytes may reach `7`), so `buf[8]`, `for (i = 0; i <= n; i++) p[i]` and `memcpy(small, src, 16)` are `out-of-bounds`, and a callee that writes `b[7]` requires eight bytes of every caller. Strings and counted fields are sizes too ([RFC 0012](docs/rfcs/0012-spatial-safety-strings-and-fields.md)): the checker knows the length of what a buffer holds (`strlen(s)`, a literal, what `strcpy`/`strcat`/`sprintf` left) and whether it is NUL-terminated at all, so `strcpy(malloc(strlen(s)), s)`, `strcat(buf, "d")` on a full `buf` and `strlen(name)` after a `strncpy` that filled `name` are `out-of-bounds`; a pointer field is sized by a sibling count, declared (`char *WEAVEC_SIZED_BY(cap) data; size_t cap;`) or inferred from every store the program makes into it, so `b->data[b->cap]` is `out-of-bounds` and `b->data = malloc(4); b->cap = 8;` is an `annotation-mismatch`; `if (i <= n - 1) a[i + 1]` and `if (i >= 8) buf[i]` are decided; and `WEAVEC_ASSUME(len < cap)` states an invariant the function cannot see. A Juliet-style recall set (`test/recall`) tracks what fraction of each CWE the checker catches. Shipped summaries for libraries beyond libc and a Clang plugin packaging are next. See [docs/roadmap.md](docs/roadmap.md). - -Opaque library objects and private state now retain inferred contracts across -source units, compiler objects and validated caches -([RFC 0028](docs/rfcs/0028-opaque-objects-and-library-state.md)). Public headers -can forward-declare supported list and buffer types: constructors establish -their actual storage, accessors preserve borrows, and cleanup invalidates saved -aliases. Explicit initialization and setters carry private scalar and callback -state without adding annotations or exposing private declarations. See the -[opaque library guide](docs/checked-code.md#opaque-objects-and-private-library-state) -for the supported boundary and required evidence, and the -[validation record](docs/validation-rfc0028.md) for closed-client proofs, -remaining limits and measured cost. - -[RFC 0029](docs/rfcs/0029-compositional-recursive-workflows.md) adds explicit -allocator/releaser callback requirements, group validation for supported recursive -cleanup, traversal and fresh construction, and buffer role discovery through -extra state fields and separate-source interfaces. Closed workflow checks cover -partial-tree failure cleanup, a streaming serializer, compiler objects and -validated cache reuse. The broader recursive parser/serializer milestone is -still in progress; see the [validation record](docs/validation-rfc0029.md). - -Checked helpers can be rechecked under established input cases, including -read-only helpers and forwarded callbacks -([RFC 0025](docs/rfcs/0025-case-sensitive-checked-contracts.md)). Named unions -with scalar or pointer members carry independent member evidence: a tag selects -a branch, while actual writes establish its payload. Complete compatible copies -preserve that evidence, and overlapping writes invalidate old values. Reports -retain each case's premises and result alongside the generic definition. See -the [case and union guide](docs/checked-code.md#check-input-cases-and-union-members) -and [validation record](docs/validation-rfc0025.md) for supported cases, -remaining limits and measured coverage and cost. - -Recursive objects have separate structural and allocation-conservation contracts -([RFC 0027](docs/rfcs/0027-recursive-object-ownership.md)). Supported finite -trees and child/sibling forests carry ownership through recursive cleanup, -attachment, detachment and ownership-preserving helper transformations. -Scalar ownership flags and borrowed backlinks retain their distinct meanings. -Discarding a child cannot count as releasing it. See the -[recursive ownership guide](docs/checked-code.md#recursive-object-ownership) -and [validation record](docs/validation-rfc0027.md) for the supported lifecycle -slice, unchanged cJSON clients and remaining limits. - -Growable buffers have inferred relational contracts -([RFC 0026](docs/rfcs/0026-growable-buffer-contracts.md)). The checker relates -current backing storage, capacity, logical length and initialized contents -across reserve, append and runtime loops. Backing ownership and pointer-element -ownership remain separate. Capacity stores do not create allocations, and -successful growth does not revive saved pointers into old storage. See the -[buffer guide](docs/checked-code.md#growable-buffers-and-vectors) for supported -operations and inference limits, and the [validation record](docs/validation-rfc0026.md) -for measured coverage and cost. - -Common C runtime operations now carry checked contracts -([RFC 0024](docs/rfcs/0024-checked-runtime-contracts.md)). Comparison and search -check initialized input; descriptor and stream reads establish only their -successful output prefix. Formatted output checks promoted argument types, -string reads, capacity and overlap. Variadic wrappers transport format and -argument-list requirements across source units, compiler objects and caches. -List copies have independent cursors, and every locally started or copied -cursor must be ended. See the [runtime guide](docs/checked-code.md#c-runtime-contracts) -for supported formats and explicit limits, including direct `va_arg`, and the -[validation record](docs/validation-rfc0024.md) for measured coverage and cost. - -Linked chains now have inferred checked contracts -([RFC 0023](docs/rfcs/0023-inductive-container-contracts.md)). Supported -traversal, runtime construction, reversal, concatenation, head detachment and -cleanup carry evidence about all remaining nodes without unrolling the list. -Borrowed stack nodes can be traversed; freeing a chain additionally requires -ownership and a matching release family for every node and owned payload. -Cycles, uninitialized links, shared owned payloads and saved aliases used after -release remain rejected. Contracts compose across helpers, source units, -compiler sidecars and validated checkpoints. See the -[container guide](docs/checked-code.md#linked-containers) and -[validation report](docs/validation-rfc0023.md) for the supported cases and -remaining limits. RFC 0027 adds complete-footprint proofs through supported -transformations. - -Constructor inference now carries the initialized heap back to callers -([RFC 0013](docs/rfcs/0013-interprocedural-heap-state.md)). If `box_new()` -allocates four bytes for `b->data`, `b->data[4]` is checked in its caller, -and `free(b)` without releasing that child reports a leak. Shared children, -argument aliases, record results and out-parameters retain their identities -across calls and files. Changing the variable used as an allocation size -does not change the allocation's bounds. The -[fixed evaluation set](test/evaluation/README.md) includes known misses; -unknown bounds and incomplete heap descriptions remain gaps in coverage. -The [corpus notes](scripts/corpus/README.md) record Lua’s remaining GC and -callback limitations, including the precision and performance tradeoffs. - -Pointer and call identity is preserved by [RFC 0014](docs/rfcs/0014-pointer-identity-and-call-effects.md). -Indirect calls use the function values that reach the call. Callback helpers -are checked under bounded bindings of those values, including across compiler -sidecars. Pointer equality and inequality guard callee effects, and complete -`memcpy`/`memmove` copies retain pointer ownership and aliases. Record paths -carry layout information so unrelated views do not acquire fabricated fields. -Unsupported copies, incompatible views and exhausted analysis limits are -visible through `analysis-incomplete`; unknown callbacks retain the existing -annotation or strict-mode boundary. The absence of diagnostics is not a -verification certificate for code outside these supported models. The -[validation report](docs/validation-rfc0014.md) records the fixed evaluation, -corpus coverage changes and increased whole-program analysis cost. - -Arrays and containers now use selected element identities ([RFC 0015](docs/rfcs/0015-array-and-container-ownership.md)). Releasing `a[1]` preserves an earlier release of `a[0]`; initialization, nullness, callback targets and ownership belong to individual pointer or record cells. Complete array `memcpy`/`memmove` operations preserve pointee identity, including overlapping moves and bounded symbolic ranges. Selected effects, range copies, returned containers and proved fill/cleanup loops compose through summaries and compiler sidecars. The representation tracks up to 32 cells and 32 range facts per storage object; unresolved selections, unsupported compositions and exhausted limits report incomplete coverage. The [validation report](docs/validation-rfc0015.md) records the improved fixed evaluation alongside corpus false positives and increased analysis cost. This remains an early static checker with explicit coverage limits. - -Helpers now preserve the safety meaning of related pointer arguments -([RFC 0016](docs/rfcs/0016-compositional-call-checking.md)). Given -`release_then_write(p, p)`, the checker follows the callee's statement order -and reports its use-after-free. Reversing the operations remains clean. -The same checking covers aliased output storage, shared record children, -selected elements, callbacks and separate compiler objects. Contexts retain -bounded caller facts; unavailable projections report incomplete coverage. -The [validation report](docs/validation-rfc0016.md) records both the added -detections and the cost and coverage warnings on real code. Calls without -established interacting identities still use generic summaries; a quiet run -does not establish that arbitrary inputs are disjoint. - -The current integer and spatial milestone -([RFC 0017](docs/rfcs/0017-c-integer-semantics-and-spatial-safety.md)) uses -the target's integer widths, promotions and conversions when checking paths, -ownership effects and buffer sizes. Narrowing, `_Bool`, mixed signedness and -unsigned wrap retain their C meaning; a definitely invalid supported operation -reports `invalid-integer-operation`. Bounded symbolic products, minimum bounds, -numeric returns and out-parameters carry sizes and conditional access -requirements through helpers and separate compiler objects. Supported -variable-length arrays retain their declaration-time bounds. Side-effecting -dimensions such as `char a[n++]` conservatively lose their captured bounds -and warn with `analysis-incomplete`; their extent and `sizeof` are not treated -as proved. Flexible-array tails use the backing allocation and target field -layout. - -`--dump-analysis` distinguishes spatial checks that are `proven`, a `violation` -or `unresolved`. Unknown bounds, unsupported expressions and exhausted limits -remain coverage gaps; general nonlinear and loop reasoning are outside the -model. Early-exit and other unsupported loops do not produce inferred -must-requirements on callers. Existing annotations remain trusted contracts. -There is no runtime instrumentation or whole-program verification certificate. -Core summary format is **25**; sidecar format **26** requires rebuilding objects carrying older -sidecars. The [validation report](docs/validation-rfc0017.md) records -**900/900 tests passing**, including under ASan/UBSan, **44/44 original bugs -detected and 32/32 clean cases**, plus twelve separate bug/clean regression -pairs. Three repeated corpus runs show the cost: median analysis time grew -from 141 to 336 seconds and peak memory grew 19%, exceeding the RFC targets. -Three new Jansson false positives and remaining coverage gaps are documented. - -Analysis can retain parsed units and immutable function preparation, reuse -specializations according to their dependencies, and share checked explanations -([RFC 0020](docs/rfcs/0020-scalable-modular-checked-analysis.md)). Optional -`--analysis-cache` checkpoints avoid function dataflow for unchanged reusable -units; `--analysis-stats` makes that work visible. Compact checked reports keep -source obligations and call routes in shared tables. See the -[incremental analysis guide](docs/incremental-analysis.md) for both command-line -spellings, input validation, report decoding and conservative cache misses. -The [RFC 0020 validation](docs/validation-rfc0020.md) records 1,029/1,029 tests -passing in Debug and ASan/UBSan, 43% less ordinary analysis time and 5% less -peak memory. All five checked corpus reports finish within 600 seconds; warm -runs reuse every unit with zero function analyses and equivalent reports. -Incomplete functions and existing checking limits remain visible. - -Checked traversal contracts ([RFC 0021](docs/rfcs/0021-practical-c-traversal.md)) -carry same-array pointer positions, consumed/produced intervals, terminated -input prefixes and paired cursor progress through helpers. Counted `while` -and `do` loops, guarded cursor advances and direct local `goto` use the same -CFG and lifetime checks. Loop facts must hold on every incoming edge; -unrelated arrays, skipped stores and overwritten terminators cannot supply -missing safety evidence. See the [traversal guide](docs/checked-code.md#check-traversals-and-cursor-helpers) -and the [validation record](docs/validation-rfc0021.md). - -Checked C interfaces ([RFC 0022](docs/rfcs/0022-checked-c-interfaces.md)) -preserve object identity through `void *`, check recovered types and alignment, -and apply the contracts of established synchronous callback targets. Allocation -hooks retain actual allocator behavior, including through private hook setters -and separate source units. Nullable output pointers can establish initialized -bytes conditional on the final pointer being non-null. These guarantees still -require valid storage, sufficient bounds and the actual callback contract; -unknown targets, incompatible views and missing initialization remain failures. -See the [interface guide](docs/checked-code.md#check-opaque-pointers-and-callback-interfaces) -and the [validation record](docs/validation-rfc0022.md). +A mostly source-compatible C compiler that brings Rust-style memory safety to existing C code through inferred ownership and borrowing. For every memory operation it compiles, WeaveC proves what it can, inserts a runtime check for the null and bounds obligations it cannot prove, and records everything else with a reason. It is built on Clang/LLVM, which does the parsing, code generation and platform support; WeaveC adds ownership inference, borrow and lifetime checking, check insertion and the safety ledger, in C++ libraries kept separate from the Clang integration. + +> **Status:** WeaveC is early, v0.x software: flags, diagnostics and on-disk formats can change between minor versions. [RFC 0030](docs/rfcs/0030-prove-or-trap.md), *Prove or trap*, defines the model described here and is being implemented; the [roadmap](docs/roadmap.md) tracks progress. ## Quick look ```c -#include #include -#include - -struct buffer *WEAVEC_OWNED buffer_new(size_t n); -size_t buffer_len(const struct buffer *WEAVEC_BORROWED b); struct node { int v; struct node *next; }; static void node_free(struct node *n) { free(n); } // inferred: consumes n @@ -216,70 +20,110 @@ static void node_free(struct node *n) { free(n); } // inferred: consumes n int example(struct node *n) { struct node *m = n; node_free(m); - return n->v; // error: use of 'n' after it was freed [weavec::use-after-free] + return n->v; // error: freed on every path } -int *escape(void) { - int x = 0; - return &x; // error: returned pointer may outlive 'x' [weavec::lifetime-too-short] +int maybe(struct node *n, int done) { + if (done) + node_free(n); + return n->v; // warning: freed on some paths } -struct node *WEAVEC_OWNED from_handle(uintptr_t h) { - WEAVEC_UNSAFE { return (struct node *)h; } // asserts ownership, at one greppable point +int *escape(void) { + int x = 0; + return &x; // error: the pointer outlives x } -int handle(uintptr_t h) { - struct node *r = (struct node *)h; // r is raw: no one knows who owns it - return r->v; // error: dereference of raw pointer 'r' outside an unsafe region [weavec::unsafe-operation] +int lookup(int i) { + static const int table[4] = {10, 20, 30, 40}; + return i < 4 ? table[i] : -1; // not proven for i < 0: checked at run time } ``` ``` $ weavec example.c -- -example.c:13:10: error: use of 'n' after it was freed [weavec::use-after-free] - 13 | return n->v; +example.c:20:11: warning: address of stack memory associated with local variable 'x' returned [-Wreturn-stack-address] + 20 | return &x; // error: the pointer outlives x + | ^ +example.c:9:10: error: use of 'n' after it was freed [weavec::use-after-free] + 9 | return n->v; // error: freed on every path | ^ -example.c:12:3: note: freed here (through 'm') - 12 | node_free(m); +example.c:8:3: note: freed here (through 'm') + 8 | node_free(m); | ^ -example.c:18:10: error: returned pointer may outlive 'x', which it points to [weavec::lifetime-too-short] - 18 | return &x; +example.c:15:10: warning: use of 'n' after it may have been freed [weavec::use-after-free] + 15 | return n->v; // warning: freed on some paths | ^ -example.c:17:7: note: 'x' is declared here - 17 | int x = 0; - | ^ -example.c:27:10: error: dereference of raw pointer 'r' outside an unsafe region [weavec::unsafe-operation] - 27 | return r->v; +example.c:14:5: note: freed here on some paths + 14 | node_free(n); + | ^ +example.c:20:10: error: returned pointer may outlive 'x', which it points to [weavec::lifetime-too-short] + 20 | return &x; // error: the pointer outlives x | ^ -example.c:26:20: note: 'r' is raw: cast from an integer here - 26 | struct node *r = (struct node *)h; - | ^ -example.c:27:10: note: move this operation into a WEAVEC_UNSAFE block or function, or assert the pointer's ownership first +example.c:19:7: note: 'x' is declared here + 19 | int x = 0; + | ^ +weavec: example.c: 11 sites: 6 proven, 1 checkable (not enforced), 2 violations, 2 unresolved, 0 trusted; 2 errors, 1 warning +2 warnings and 2 errors generated. +Error while processing example.c. ``` -Annotations (`WEAVEC_OWNED`, `WEAVEC_BORROWED`, `WEAVEC_MUT`, `WEAVEC_RAW`, `WEAVEC_UNSAFE`, `WEAVEC_NULLABLE`, `WEAVEC_NONNULL`, `WEAVEC_RETAINS`, `WEAVEC_RELEASES`, `WEAVEC_REFCOUNT`, `WEAVEC_OWNED_BY(f)`) expand to nothing on other compilers, so annotated code remains plain, portable C. See [docs/annotations.md](docs/annotations.md). +Definite bugs are errors; a use-after-free on some paths only is a warning. The first warning is Clang's own. The last line summarises the file's *ledger*, which records an outcome for each safety facet (spatial, null, temporal) of every memory operation (*site*): proven, checked, a violation, or unresolved or trusted with a reason. The line counts each site by its worst facet. `table[i]` is counted as checkable: `weavec` only analyses, and `weavec-cc`, the compiler, turns it into a check that traps when `i` is negative. + +Annotations (`WEAVEC_OWNED`, `WEAVEC_BORROWED`, `WEAVEC_MUT`, `WEAVEC_RAW`, `WEAVEC_UNSAFE`, `WEAVEC_NULLABLE`, `WEAVEC_NONNULL`, `WEAVEC_COUNTED_BY(n)`, `WEAVEC_ENDED_BY(q)`, `WEAVEC_STRING`, `WEAVEC_REQUIRE_SAFE`, `WEAVEC_ASSUME(e)` and the reference-counting forms) state contracts where inference needs help. They expand to nothing on other compilers, so annotated code remains plain, portable C. See [docs/annotations.md](docs/annotations.md). + +## What WeaveC guarantees + +For a translation unit compiled by `weavec-cc` in an enforcing mode (the default `-fweavec-checks=trap`, or `verify`, with zero-initialisation on), every operation outside a `WEAVEC_UNSAFE` region satisfies: + +- **(S)** if its spatial facet is proven or checked, it accesses only bytes inside the object its pointer was derived from, or the program traps first; +- **(N)** if its null facet is proven or checked, it does not dereference null, or the program traps first; +- **(T)** if its temporal facet is proven, the object is still alive, and a release releases a live allocation once; +- **(V)** a definite violation never reaches the object unguarded: it fails the build, or, if lowered with `-Wno-error`, traps. + +These hold under five assumptions: **A1** callers outside the unit pass arguments that meet what it relies on; **A2** trusted callees (platform functions, the library table, declared contracts, code without WeaveC records) behave as their contracts say; **A3** other code leaves reachable pointers null or pointing to live objects, with owners unique; **A4** no other thread, signal handler or `longjmp` changes the memory outside sites marked for it; **A5** the allocator answers its usable-size query consistently, and memory from sources WeaveC does not zero is written before pointers are read from it. If a memory-safety violation happens anyway, then a check trapped first, or the ledger shows an unresolved or trusted facet (or an assumption at the unit's interface) that it rests on, or WeaveC has a bug, which `verify` mode monitors. Temporal bugs are not checked at run time. The full statement, what is caught and what is not, is in [the guarantees reference](docs/pages/reference/guarantees.md) and [RFC 0030, *Soundness*](docs/rfcs/0030-prove-or-trap.md#soundness). + +## Modes + +| `-fweavec-checks=` | Unproven null and bounds obligations | Zero-init | Guarantee | +| --- | --- | --- | --- | +| `trap` (default) | checked; a failed check traps | on | yes | +| `report` | checked; a failed check prints `weavec: runtime check failed: …` and continues (links `libweavec_rt.a`) | on | only with `WEAVEC_RT_ABORT=1` | +| `verify` | checked; proven facets are also checked where expressible, so a `weavec.proven` trap exposes a wrong proof | on | yes | +| `none` | nothing: the object is what Clang would produce | off | no | + +- **Zero-initialisation.** In the checking modes, locals and the standard allocation calls are zero-initialised, so an uninitialised pointer is null and its checked dereference traps. `-fno-weavec-zero-init` turns it off. +- **Require levels.** `-fweavec-require=checked` makes every unresolved facet an `unresolved-operation` error; `-fweavec-require=proven` also makes every checked facet an `unchecked-operation` error. Trusted facets are allowed at every level. `WEAVEC_REQUIRE_SAFE` holds one function to `checked`. +- **Ledger.** `-fweavec-ledger=` writes every site and facet with its outcome, reason, fix-it and a stable fingerprint, as JSON or, with `-fweavec-ledger-format=sarif`, SARIF 2.1.0. `-fweavec-summary` prints the one-line summary, which `weavec` always prints. ## Using it as the compiler -`weavec-cc` is Clang's driver with WeaveC inside. Point a build at it and it compiles as `clang` would, analyses each file as it compiles it, and checks the whole program when it links: +`weavec-cc` is Clang's driver with WeaveC inside. Point a build at it and it compiles as `clang` would, analyses and instruments each file as it compiles it, and checks the whole program when it links: ```sh -$ CC=weavec-cc make -weavec-cc -c node.c -o node.o # node.o and node.o.weavec (its summaries) +$ make CC=weavec-cc +weavec-cc -c node.c -o node.o # node.o and node.o.weavec (its WeaveC record) weavec-cc -c main.c -o main.o -weavec-cc node.o main.o -o prog # reads the sidecars, analyses the program, then links -main.c:8:3: error: 'n' is freed twice [weavec::double-free] - 8 | node_free(n); - | ^ -main.c:7:3: note: previously freed here - 7 | node_free(n); - | ^ -1 error generated. +weavec-cc node.o main.o -o prog # reads the records, analyses the program, then links +``` + +A bug inside one file is reported when that file is compiled; a bug that needs two files is reported when they are linked, and an error stops the link. Link inputs without a WeaveC record (archives, shared libraries, objects from another compiler) are named in one `unanalyzed-input` warning. + +The checks are ordinary C inserted before code generation, with no ABI change and no runtime library in the default mode. With `lookup` from the quick look in a program that passes it `atoi(argv[1])`: + +``` +$ weavec-cc -fweavec-summary lookup.c -o lookup +weavec: lookup.c: 7 sites: 5 proven, 2 checked, 0 unresolved, 0 trusted; 0 errors, 0 warnings +weavec: program lookup: 7 sites in 1 unit: 5 proven, 2 checked, 0 unresolved, 0 trusted; 0 errors, 0 warnings; unverified: 0 exported requirements (A1), 0 header invariants (A3) +$ ./lookup 2 +30 +$ ./lookup -1; echo "exit status $?" +exit status 133 ``` -A bug inside one file is reported when that file is compiled; a bug that needs two files (`node_free` is defined in `node.c`) is reported when they are linked, and an error stops the link. Flags: `-fno-weavec` (compile only), `-fweavec-strict` (every call into unknown code is a raw operation), `-fno-weavec-link` (skip the link-time step), `-Wno-weavec-annotation-required`, `-Wno-error=weavec-use-after-free` (lower an error to a warning while migrating), `-Werror=weavec`. +The negative index stops the program with `SIGTRAP` (or `SIGILL`, depending on the target) at the access, instead of reading past the table. Other flags: `-fno-weavec` (plain Clang), `-fno-weavec-link` (skip the link-time step), `-fweavec-budget=` (per-function analysis budget), `-Wno-error=weavec-` (lower an error to a warning while migrating), `-Werror=weavec`. `weavec-cc --help-weavec` lists them all. -The tooling form analyses a compilation database without building: `weavec --whole-program -p build/` (all sources) or `weavec --whole-program a.c b.c -- -Iinclude`. Without `--whole-program`, `weavec file.c --` checks one file as before. +The tooling form analyses a compilation database without building: `weavec --whole-program -p build/` (all sources) or `weavec --whole-program a.c b.c -- -Iinclude`. Without `--whole-program`, `weavec file.c --` checks one file. Both take `--ledger`, `--ledger-format` and `--require`. ## Building @@ -298,7 +142,7 @@ export WEAVEC_LLVM_PREFIX=/usr/lib/llvm-23 # Everyone cmake --preset dev # configure into build/dev cmake --build --preset dev # build -ctest --preset dev # run unit + integration tests +ctest --preset dev # unit, lit and test/cases suites, in parallel ``` Other presets: `dev-asan`, `dev-tidy`, `release`, `relwithdebinfo`. The full list is in [`CMakePresets.json`](CMakePresets.json); the developer guide is [docs/development.md](docs/development.md). @@ -307,14 +151,11 @@ Other presets: `dev-asan`, `dev-tidy`, `release`, `relwithdebinfo`. The full lis [GitHub Releases](https://github.com/weavefoundry/weavec/releases) is the distribution channel for WeaveC. Initial 0.x releases provide -`weavec-X.Y.Z-source.tar.gz` and `SHA256SUMS`. They are early checker releases -with the coverage limits described above; APIs and on-disk formats can change -between minor versions. +`weavec-X.Y.Z-source.tar.gz` and `SHA256SUMS`. They are early releases (see +*Status* above); APIs and on-disk formats can change between minor versions. The first release creates `CHANGELOG.md` from Conventional Commits; later releases regenerate it from the commit history. -The earlier hand-written implementation and migration notes are preserved in -[the development history](docs/development-history.md). Download both files into the same directory and verify the archive with `shasum -a 256 -c SHA256SUMS` (or `sha256sum -c SHA256SUMS` on Linux). @@ -341,20 +182,26 @@ selection, publication and retries. ``` include/weavec/ Public C++ headers - Core/ Ownership lattice, lifetimes, borrows, moves, diagnostics (no Clang/LLVM) - Analysis/ Clang AST -> core facts; the checkers - Frontend/ Clang FrontendAction / libTooling integration -lib/ Implementations, mirroring include/ + Core/ Ownership lattice, lifetimes, borrows, moves, pointer kinds, the ledger, + the library table, check plans, diagnostics (no Clang/LLVM) + Analysis/ Clang AST -> core facts: sites, kinds, the engine and the planner behind one seam + Frontend/ Clang integration: deferred CodeGen, check emission, zero-init, ledger writers, + unit records, the whole-program step, the compiler driver +lib/ Implementations, mirroring include/ (lib/Core/LibrarySpec.txt is the library table) +runtime/ The small C runtime: report-mode reporting and out-of-line check helpers tools/weavec/ The analysis tool (libTooling; --whole-program for a compilation database) tools/weavec-cc/ The drop-in compiler driver (Clang's driver with WeaveC inside) resources/ weavec.h, the C-facing annotation header (installed to lib/weavec/include) unittests/ GoogleTest unit tests test/ lit + FileCheck integration tests -docs/ Architecture, RFCs (docs/rfcs/), roadmap + cases/ Executable C cases by feature, with markers, run by scripts/run-cases.py + corpus/ Real projects pinned by SHA, expectations and triage, run by scripts/corpus-gate.py +scripts/ Test runners, the corpus gate, hygiene and release tooling +docs/ Architecture, RFCs (docs/rfcs/), roadmap, and the weavec.com site cmake/ Build-system modules ``` -The layering rule is strict: `Core` must not include anything from `clang/` or `llvm/`. `Analysis` is the only layer that knows about both worlds. See [docs/architecture.md](docs/architecture.md). +The layering rule is strict: `Core` must not include anything from `clang/` or `llvm/`. `Analysis` is the only layer that knows about both worlds, and only the engine behind the `SafetyEngine` seam sees the dataflow internals. See [docs/architecture.md](docs/architecture.md). ## Contributing diff --git a/docs/README.md b/docs/README.md index b23bc27..ac79886 100644 --- a/docs/README.md +++ b/docs/README.md @@ -33,7 +33,6 @@ content. Author new site-specific content in `pages/`. - [Developer guide](development.md) - [Architecture](architecture.md) - [Annotations and diagnostics](annotations.md) -- [Checked code](checked-code.md) - [RFCs](rfcs/README.md) - [Roadmap](roadmap.md) diff --git a/docs/annotations.md b/docs/annotations.md index 34be0f2..f0dcc52 100644 --- a/docs/annotations.md +++ b/docs/annotations.md @@ -1,7 +1,8 @@ # Annotations reference -WeaveC annotations live in the `weavec.h` header, which `weavec` puts on the -system include path automatically (`#include `). Every macro expands +WeaveC annotations live in the `weavec.h` header, which `weavec` and +`weavec-cc` put on the system include path automatically +(`#include `). Every macro expands to `__attribute__((annotate("weavec.")))` under Clang and to nothing under compilers without the `annotate` attribute, so annotated code stays portable C. @@ -12,15 +13,19 @@ portable C. | `WEAVEC_BORROWED` | pointer parameters, returns, variables, fields | Shared, read-only borrow. The referent outlives the borrow. | | `WEAVEC_MUT` | pointer parameters, returns, variables, fields | Exclusive, mutable borrow. | | `WEAVEC_RAW` | pointer parameters, returns, variables, fields, function-pointer types | No guarantee at all: the checker tracks the pointer but any dereference, release or transfer of ownership must happen inside a `WEAVEC_UNSAFE` region. | -| `WEAVEC_UNSAFE` | function declarations, compound statements | An *unsafe region*: raw operations are permitted and nothing inside is reported, but ownership still flows through it and out of it. | +| `WEAVEC_UNSAFE` | function declarations, compound statements | An *unsafe region* ([RFC 0030](rfcs/0030-prove-or-trap.md) §6.1): raw pointers and spatial and null operations inside it are trusted, and no runtime checks are inserted there. Temporal state is still tracked: possible temporal findings are warnings as elsewhere, and definite violations remain errors. Ownership still flows through it and out of it. | | `WEAVEC_NULLABLE` | pointer parameters, returns, variables, fields | The pointer may be null ([RFC 0008](rfcs/0008-pointer-validity.md)). On a parameter: the body must test it before dereferencing it, and callers may pass null. On a return type: callers must test the result. On a variable or field: every load is treated as maybe-null until it is tested. Says nothing about ownership; combine with `WEAVEC_OWNED`/`WEAVEC_BORROWED`/`WEAVEC_MUT` as needed. | -| `WEAVEC_NONNULL` | pointer parameters, returns, variables, fields | The pointer is never null ([RFC 0008](rfcs/0008-pointer-validity.md)). On a parameter: callers must pass a pointer the checker knows is non-null, even if the body never dereferences it. On a return type: callers need not test the result. On a variable or field: it is never reported as null. Says nothing about ownership. | +| `WEAVEC_NONNULL` | pointer parameters, returns, variables, fields | The pointer is never null ([RFC 0008](rfcs/0008-pointer-validity.md)). On a parameter: an argument that may be null is checked at the call ([RFC 0030](rfcs/0030-prove-or-trap.md)), and a definitely null one is an error, even if the body never dereferences it. On a return type: callers need not test the result. On a variable or field: it is never reported as null. Says nothing about ownership. | | `WEAVEC_RETAINS` | pointer parameters | The callee takes a reference on the argument's object ([RFC 0010](rfcs/0010-shared-ownership.md)): the caller's pointer gains a *share*, which the next copy of it carries away. On a declaration with no body whose result has the parameter's type and no ownership annotation, the result is a copy of the argument (the shape of `g_object_ref`). | | `WEAVEC_RELEASES` | pointer parameters | The callee releases one reference ([RFC 0010](rfcs/0010-shared-ownership.md)): the argument's name is dead afterwards; other shares of the object are untouched. | | `WEAVEC_REFCOUNT` | integer fields | The field is a reference count ([RFC 0010](rfcs/0010-shared-ownership.md)): a share taken through it and never released is a `leak` even when no function in the program releases through it. Inference recognises the field by its increments and decrements regardless. | | `WEAVEC_OWNED_BY(f)` | pointer parameters and returns, next to `WEAVEC_OWNED` | The release family is `f` ([RFC 0010](rfcs/0010-shared-ownership.md)): `struct handle *handle_open(void) WEAVEC_OWNED WEAVEC_OWNED_BY(handle_close);` makes `free(handle_open())` a `mismatched-release`. Without `WEAVEC_OWNED` it is an `invalid-annotation`. | -| `WEAVEC_SIZED_BY(n)` | pointer parameters, pointer fields | On a parameter: the caller passes at least `n` elements behind the pointer (bytes for `void *`), `n` being another parameter of the same function by name ([RFC 0011](rfcs/0011-spatial-safety.md)): `void fill(char *WEAVEC_SIZED_BY(len) buf, size_t len);`. Inside the body the parameter has that extent, so `buf[len]` is `out-of-bounds`; at every call the argument must have at least that many, so `fill(small, 8)` on `char small[4]` is `out-of-bounds`. On a field: the object holds at least `n` elements behind the pointer, `n` being another integer field of the same struct by name ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)): `struct buf { char *WEAVEC_SIZED_BY(cap) data; size_t cap; };`. Every function that loads the field sees that extent (`b->data[b->cap]` is `out-of-bounds`, `for (i = 0; i <= b->cap; i++) b->data[i]` may be), and a store into the field of an object the count says is too small is an `annotation-mismatch` (`b->data = malloc(4); b->cap = 8;`, in either order). Says nothing about ownership or nullness; combine with the others as needed. On a non-pointer, or naming a parameter or field that does not exist or is not an integer: `invalid-annotation`. | -| `WEAVEC_ASSUME(expr)` | statements | `expr` holds from here on, as if the code below were inside `if (expr)` ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)): `WEAVEC_ASSUME(b->len < b->cap);` lets the checker prove `d[b->len]` in bounds on `malloc(b->cap)`, `WEAVEC_ASSUME(p != NULL)` removes a `null-dereference`. Trusted like every annotation: an assumption the checker's facts contradict ends the path (nothing below it is analysed), and a false one hides reports. `expr` must be side-effect free; it is evaluated under WeaveC and is an unevaluated operand (`sizeof`) under every other compiler. | +| `WEAVEC_SIZED_BY(n)` | pointer parameters, pointer fields | A synonym of `WEAVEC_COUNTED_BY(n)` ([RFC 0030](rfcs/0030-prove-or-trap.md) §7.2): `n` counts elements (bytes for `void` and character pointees), unlike Clang's byte-counting `sized_by`. It keeps its [RFC 0011](rfcs/0011-spatial-safety.md) and [RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md) meaning (`void fill(char *WEAVEC_SIZED_BY(len) buf, size_t len);`, `struct buf { char *WEAVEC_SIZED_BY(cap) data; size_t cap; };`): inside the body the parameter has that extent, so `buf[len]` is `out-of-bounds`; a call with a smaller object is `out-of-bounds`; a store into the field of an object the count says is too small is an `annotation-mismatch`. Calls and accesses through the pointer that are not proven are checked at run time. New code should use `WEAVEC_COUNTED_BY`. On a non-pointer, or naming nothing or a non-integer: `invalid-annotation`. | +| `WEAVEC_COUNTED_BY(n)` | pointer parameters, pointer fields | At least `n` elements (bytes for `void` and character pointees) are accessible from the pointer: the kind `counted(n)` (`sized(n)`) of [RFC 0030](rfcs/0030-prove-or-trap.md) §7.2. `n` names a sibling parameter or field by name, in any position, so the count may follow the pointer (`void fill(char *WEAVEC_COUNTED_BY(len) buf, size_t len);`, `struct buf { char *WEAVEC_COUNTED_BY(cap) data; size_t cap; };`). The kind is checked at every call and every store, and accesses through the pointer are proven against it or checked at run time. A name that resolves to nothing or to a non-integer is an `invalid-annotation`, and the kind is dropped. | +| `WEAVEC_ENDED_BY(q)` | pointer parameters, pointer fields | `[p, q)` lies in one object, `q` naming a sibling pointer parameter or field by name, in any position: the kind `ended-by(q)` ([RFC 0030](rfcs/0030-prove-or-trap.md) §7.2). `size_t sum(const int *WEAVEC_ENDED_BY(end) p, const int *end);`. A name that resolves to nothing or to a non-pointer is an `invalid-annotation`. | +| `WEAVEC_STRING` | pointer parameters, returns, fields | The pointer is NUL-terminated within its object (a zero element lies at or after it): the kind `nul-terminated` ([RFC 0030](rfcs/0030-prove-or-trap.md) §7.2). `size_t name_len(const char *WEAVEC_STRING name);`. On a non-pointer or a variable: `invalid-annotation`. | +| `WEAVEC_REQUIRE_SAFE` | function definitions | Holds the function's operations to `-fweavec-require=checked` whatever the command line says ([RFC 0030](rfcs/0030-prove-or-trap.md) §6.3): each must be proven safe or guarded by a runtime check, and anything else is an `unresolved-operation` error. `WEAVEC_REQUIRE_SAFE int parse(const char *WEAVEC_STRING s) { ... }`. It replaces `WEAVEC_CHECKED`, which `weavec.h` no longer defines. On anything but a function: `invalid-annotation`. | +| `WEAVEC_ASSUME(expr)` | statements | `expr` holds from here on, as if the code below were inside `if (expr)` ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)): `WEAVEC_ASSUME(b->len < b->cap);` lets the checker prove `d[b->len]` in bounds on `malloc(b->cap)`. The assumption itself is not trusted ([RFC 0030](rfcs/0030-prove-or-trap.md) §6.2): when the analysis proves `expr` nothing is added; when it refutes it, that is a `contradicted-assumption` error; otherwise `weavec-cc` replaces the call with a runtime assertion that traps when `expr` is false. The analysis assumes `expr` after it in every case. `expr` must be side-effect free; it is evaluated under WeaveC and is an unevaluated operand (`sizeof`) under every other compiler. | | `WEAVEC_ENABLED` | (macro, not an attribute) | `1` when the TU is being processed by `weavec`, else `0`. | Annotations on a function-pointer type describe whatever is called through it @@ -39,12 +44,16 @@ An annotation on the declarator of a function pointer (the typedef name, the field or the parameter) describes the *result* of calls through it; the annotations inside its parameter list describe the arguments. -Without a type contract, calls use the actual function-pointer values that -reach them ([RFC 0014](rfcs/0014-pointer-identity-and-call-effects.md)). A helper -can be checked with distinct callback bindings; a same-type function elsewhere -in the program does not provide an unknown callback's behavior. Global target -values include possible writes from analyzed functions, while a known store -at a call updates that caller's state. Unknown alternatives remain boundaries. +Without a type contract, a call through a function pointer uses the functions +the program stores into that pointer's *slot* (a field, global, parameter or +result; [RFC 0030](rfcs/0030-prove-or-trap.md) §9.3): one known target is +analysed as a direct call, several as the join of their summaries. A +same-type function elsewhere in the program does not provide an unknown +callback's behavior. A slot that can also receive values from outside the +program keeps its known targets for temporal facts, trusted as +`extern-contract`; a slot with no known target is treated as an unknown +callee, with reason `callback`. `weavec --whole-program` and the link step +solve the slots across units. ## Placement @@ -72,21 +81,24 @@ WEAVEC_UNSAFE void poke_hardware(volatile uint32_t *reg) { *reg = 1; } For blocks, before the opening brace: ```c -void f(int *p) { - free(p); +void reset_device(uintptr_t base) { WEAVEC_UNSAFE { - /* p is dangling here; we know the allocator keeps the page mapped. */ - log_address(p); + /* base is the device's mapped register block. */ + *(volatile uint32_t *)base = 1; } } ``` -An unsafe region is a boundary, not a hole: the checker still analyses what -happens inside it (so a `free` inside the block is a free as far as the code -after it is concerned, and the function's summary is still inferred) and only -stops *reporting* there. It is also the only place a `WEAVEC_RAW` pointer may -be dereferenced, released or handed to an owning parameter, and the place to -assert what a raw pointer really is: +An unsafe region is a boundary, not a hole ([RFC 0030](rfcs/0030-prove-or-trap.md) +§6.1). The checker still analyses what happens inside it: a `free` inside the +block is a free as far as the code after it is concerned, and the function's +summary is still inferred. Inside the region, spatial and null operations +and raw pointers are trusted (`trusted(unsafe)` in the ledger) and get no +runtime checks. Nothing is suppressed: temporal findings are reported as +anywhere else, definite violations remain errors, and `WEAVEC_ASSUME` keeps +its runtime assertion. The region is also the only place a `WEAVEC_RAW` +pointer may be dereferenced, released or handed to an owning parameter, and +the place to assert what a raw pointer really is: ```c struct node *WEAVEC_OWNED node_from_handle(uintptr_t h) { @@ -109,9 +121,7 @@ cascade. See [RFC 0004](rfcs/0004-unsafe-boundaries.md), *Laundering*. results and function-pointer results); - a load through a raw pointer (`raw->next` is raw too); - the result of a callee whose body returns or stores a raw value, or whose - declaration says `WEAVEC_RAW`; -- under `--strict-externs`, every pointer that passes through a call the - checker cannot resolve (see `annotation-required`). + declaration says `WEAVEC_RAW`. Copying, comparing and converting a raw pointer back to an integer are fine anywhere; passing it to a callee's `WEAVEC_RAW` parameter is fine too. Only a @@ -122,65 +132,68 @@ callee that reads or writes through it is a *raw operation*. Every WeaveC diagnostic ends with a stable identifier in brackets, e.g. `[weavec::use-after-free]`. The IDs are defined in -`include/weavec/Core/Diagnostic.h`; RFC 0017 adds -`weavec::core::diag::InvalidIntegerOperation`, spelled -`invalid-integer-operation`, with error severity. +`include/weavec/Core/Diagnostic.h`. Severity follows certainty +([RFC 0030](rfcs/0030-prove-or-trap.md) §3): a finding that holds on every +path is an error, and a temporal finding that holds on some paths only is a +warning with "may" wording. A null dereference or out-of-bounds access that +is only possible is not diagnosed: the operation is a *checked* facet, and +`weavec-cc` inserts a runtime check for it. RFC 0030 removed +`analysis-incomplete`, `annotation-required`, `checking-incomplete` and +`checking-failed`; what they reported is now an `unresolved` ledger row with +a reason. | Identifier | Severity | Emitted when | | --------------------- | -------- | --------------------------------------------------------------------- | -| `checking-incomplete` | error | A selected function has an unresolved safety obligation: `cannot establish checked safety: `. | -| `checking-failed` | error | A selected function contains a demonstrated violation: `checked safety failed: `. | -| `use-after-free` | error | A pointer (or any alias of it) is used after being passed to `free`. Note: `freed here` / `freed here (through '')`. After a share release ([RFC 0010](rfcs/0010-shared-ownership.md)): `use of '

' after its reference was released`, note `reference released here`. | -| `double-free` | error | A pointer (or any alias of it) is passed to `free` twice without reassignment. Note: `previously freed here [(through '')]`. Two share releases of one name ([RFC 0010](rfcs/0010-shared-ownership.md)): `'

' is released twice`, note `previously released here`. | -| `use-after-move` | error | A pointer is used after being passed to a `WEAVEC_OWNED` parameter, to `realloc`, or to a function that moves it (on every path, or on the paths whose result the caller has not ruled out; [RFC 0006](rfcs/0006-precision.md)). Note: `moved here`. | -| `conflicting-borrow` | error | An object is freed or moved while a live pointer into it exists: `cannot free '

' while it is borrowed`, `cannot move '

' while it is borrowed`. Note: `borrowed by '' here`. A pointer is *live* until its last use ([RFC 0006](rfcs/0006-precision.md)). Not reported for a pointer *derived* from `

` (`q = &p->f`, `q = p + 1`): that is a name for the same object, and its later use is a `use-after-free` ([RFC 0011](rfcs/0011-spatial-safety.md)). With `--exclusive-borrows` (`-fweavec-exclusive-borrows`), RFC 0001's exclusivity rules are enforced too: `cannot borrow '' as mutable because it is already borrowed`, `... as shared because it is already mutably borrowed`, `cannot assign to '' while it is borrowed`; the note names the other pointer. | -| `lifetime-too-short` | error | A pointer may outlive what it points to: `'

' may outlive '', which it points to` (stored into an outer scope, a global or through a parameter) or `returned pointer may outlive '', which it points to`. Notes: where `` is declared and where it goes out of scope. Reported at the store, but decided when `` dies ([RFC 0011](rfcs/0011-spatial-safety.md)): a store undone before then (`ls->fs = fs.prev`), or into a holder that is dead by then, is not reported. | -| `unsafe-operation` | error | A raw operation outside a `WEAVEC_UNSAFE` region ([RFC 0004](rfcs/0004-unsafe-boundaries.md)): `dereference of raw pointer '

' outside an unsafe region`, `'' dereferences raw pointer '

' ...` (also `releases`, `takes ownership of`), `raw pointer '

' is assigned to '', which is declared WEAVEC_OWNED, outside an unsafe region` (any safe annotation), `raw pointer is returned from a function whose return type is annotated WEAVEC_OWNED outside an unsafe region`, and with `--strict-externs`, `unchecked call to '' outside an unsafe region` / `unchecked call through '' ...`. Notes: why the pointer is raw (`'

' is raw: cast from an integer here`, `declared WEAVEC_RAW here`, `loaded through raw pointer '' here`, `handed out by '' here`, `returned by a call into unchecked code ('') here`, each optionally `(through '')`) and `move this operation into a WEAVEC_UNSAFE block or function, or assert the pointer's ownership first`. | -| `mismatched-release` | error | A resource is released (or moved into a consuming parameter) by a function of another release family ([RFC 0007](rfcs/0007-resource-lifecycle.md)): `'

' is released with 'free' but must be released with 'fclose'`. Both names are family names, the canonical releaser of the allocator (`malloc`/`strdup`/`realloc` → `free`, `fopen` → `fclose`, `opendir` → `closedir`, ...), even when the release went through a wrapper defined in the program. Note: `allocated here`. | -| `leak` | warning | An owned resource is lost without being released, moved or stored where the caller can see it ([RFC 0007](rfcs/0007-resource-lifecycle.md)): `'

' is leaked` at the point its last holder goes out of reach (a `return`, a scope end, the statement after its last use); `'

' is leaked: it is overwritten without being released` at the assignment; `'->p' is leaked when '' is freed` (also `'*a' is leaked when 'a' is freed`) at the release of a container whose `WEAVEC_OWNED` field, or a field this function stored an owned value into, still owns something; `result of '' is leaked` at a discarded allocating call. Notes: `allocated here`, `'

' is declared WEAVEC_OWNED here` for a parameter or field, or `reference taken here` for a share retained by a count increment and dropped ([RFC 0010](rfcs/0010-shared-ownership.md); reported only through a *known count*: a field some function in the program releases through, or one annotated `WEAVEC_REFCOUNT`). Not reported: pointers handed to callees the checker cannot follow or cast to integers (they are *escaped*), resources kept by globals or `static` locals when the function returns, blocks that end in a `noreturn` call, fields of an object this function allocated, and the old block after a failed in-place `realloc`. | -| `null-dereference` | error | A pointer that is null, or may be null, on some path reaching here is dereferenced ([RFC 0008](rfcs/0008-pointer-validity.md)): `dereference of '

', which may be null` / `dereference of '

', which is null`; or passed to a callee that dereferences its parameter without testing it (a `requires` fact in the callee's summary, or `WEAVEC_NONNULL` on its declaration): `'

', which may be null, is passed to '', which dereferences it` (also `which is null`, `a null pointer is passed to '' ...`). The note says why: `'

' may be null: it is the result of '' here` (every allocator in the shipped table, every searching function and every function the program defines whose body can return null), `'

' may be null: it is set by '' here` (a callee's store), `'

' is assigned NULL here`, `'

' may be null: it is compared with NULL here` (tested, and the null edge merged back), `'

' is declared WEAVEC_NULLABLE here` / `the result of '' is declared WEAVEC_NULLABLE here`; for a call, also `'' is declared here`. Not reported: pointers with no fact (parameters, loaded fields, results of unchecked code), dereferences inside an unsafe region, and a second dereference of the same pointer. | -| `use-of-uninitialized`| error | 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 ([RFC 0008](rfcs/0008-pointer-validity.md)): `use of '

' before it was initialized` (also `'.f'`). Note: `'

' is declared here`. Any assignment, a callee's store (`init(&p)`), a mutable borrow for a call, `memset` or a whole-object write initialises it; `static` and address-taken variables are not tracked. | -| `invalid-release` | error | A releaser (or a consuming parameter) is handed a pointer that is not the start of a heap allocation ([RFC 0008](rfcs/0008-pointer-validity.md)): `'

' is released but points to '', which is not a heap object` (a stack or static variable, an array, a field of one; `'' is released but is not a heap object` when `

` is `` itself), `'

' is released but points to a string literal`, `'

' is released but points 4 elements past the start of its allocation` / `points to field 'in' of its allocation` / `does not point to the start of its allocation` (`p + 1`, `strchr(p, c)`, `p++`, `&o->in`; the offset is named when the checker knows it, [RFC 0011](rfcs/0011-spatial-safety.md)). Notes: `'' is declared here` / `allocated here`. | -| `out-of-bounds` | error | An access reaches past the object it is in, or before its start ([RFC 0011](rfcs/0011-spatial-safety.md)). Direct accesses: `'

[]' is out of bounds: index of an object of bytes` (both constant; the index is spelled as written, with its folded value in parentheses when that differs), `'

[]' is out of bounds: '' is the number of elements of '

'` / `'' is at least '', the number of elements of '

'` / `'' is above '', ...` (the index related to the count by a condition), `'

[]' may be out of bounds: '' may equal '', the number of elements of '

'` (`i <= n`: the boundary is one past) / `'' may reach one below '', and '

' has * 4 bytes` (`p[i + 1]` under `i < n`), `'

[]' may be out of bounds: '' may be 7 in an object of 4 bytes` (the index bounded above by a constant: `for (i = 0; i < 8; i++)`), `'

[]' is out of bounds: index is before the start of '

'`. Library calls with a buffer and a length (`memcpy`, `memmove`, `memset`, `memcmp`, `fgets`, `snprintf`, `read`, `write`, `strncpy`, ...): `'memcpy' accesses 16 bytes of '

', which has 8 bytes` and the relational forms (`'memset' accesses 'm' bytes of 'p', which has 'n' bytes ('m' is above 'n')`, `'memset' may access past the end of 'buf': 'n' may be 8, and 'buf' has 4 bytes`). A callee's requirement at the call: `'put7' requires 8 bytes behind '

', which has 4 bytes`. Notes: `'

' is allocated here` / `'

' is declared here` / `the object behind '

' is declared here`. Extents come from allocations (`malloc(n)`, `calloc(n, sz)`, `realloc(p, n)`, and every function in the program that returns one: `xmalloc(n)` returns `fresh extent=n`), from the declared size of a variable, an array or an array member, from string literals, from `WEAVEC_SIZED_BY` on a parameter, and from the count of a sized field ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)), declared or inferred (`'b->data[b->cap]' is out of bounds: 'b->cap' is the number of elements of 'b->data'`, note `'b->data' is declared here`). Strings (RFC 0012): a copy that needs the length plus the terminator is checked like a length (`'strcpy' accesses 6 bytes of 'buf', which has 4 bytes`, `'strcpy' accesses 'strlen(s)' + 1 bytes of 'd', which has 'strlen(s)' bytes` on `malloc(strlen(s))`, `'strcat' accesses 5 bytes of 'buf', which has 4 bytes` counting what `buf` already holds, `'sprintf' accesses at least 5 bytes of 'buf', which has 4 bytes` from the format's minimum), and a terminator-seeking read (`strlen`, `strcpy`'s source, `strcat`'s, `puts`, `printf("%s")`) of an object the checker knows has no terminator (`strncpy` that filled it, `char a[4] = "abcd"`, `memset(a, 'x', sizeof a)`) is `'strlen' reads past the end of 'name', which is not NUL-terminated`, note `'name' is left without a terminator here`. Relations one step further (RFC 0012): `'a[i + 1]' may be out of bounds: 'i' may reach one below 'n', and 'a' has 'n' * 4 bytes` under `i <= n - 1`, `'buf[i]' is out of bounds: 'i' is at least 8 in an object of 8 bytes` under `i >= 8`. RFC 0017 also checks actual converted or wrapped allocation sizes, represented products, VLA dimensions and allocated flexible-array tails; a dimension violation can say `'' is out of bounds for its variable array dimension`, and a caller interval can say `'' requires '

' before its start`. Unresolved indices, unknown sizes or offsets, unsupported field layouts and unknown string lengths do not by themselves produce this error or establish safety. | +| `use-after-free` | error / warning | A pointer (or any alias of it) is used after being passed to `free`. An error when the release happened on every path to the use; otherwise a warning with "may" wording ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.1): `use of '

' after it may have been freed`, note `freed here on some paths`. Note: `freed here` / `freed here (through '')`. After a share release ([RFC 0010](rfcs/0010-shared-ownership.md)): `use of '

' after its reference was released` (`... may have been released`), note `reference released here`. A release by code WeaveC cannot see (an unknown callee, inline assembly) is never reported: the use is an `unresolved(unknown-callee)` ledger row (§5.1). | +| `double-free` | error / warning | A pointer (or any alias of it) is passed to `free` twice without reassignment: `'

' is freed twice`, or, when the first release happened on some paths only, `'

' may be freed twice` ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.1). Note: `previously freed here [on some paths] [(through '')]`. Two share releases of one name ([RFC 0010](rfcs/0010-shared-ownership.md)): `'

' is released twice` (`may be released twice`), note `previously released here`. | +| `use-after-move` | error / warning | A pointer is used after being passed to a `WEAVEC_OWNED` parameter, to `realloc`, or to a function that moves it (on every path, or on the paths whose result the caller has not ruled out; [RFC 0006](rfcs/0006-precision.md)). Note: `moved here`. On some paths only: `use of '

' after it may have been moved`, a warning ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.1). | +| `conflicting-borrow` | error / warning | An object is freed or moved while a live pointer into it exists: `cannot free '

' while it is borrowed`, `cannot move '

' while it is borrowed`. Note: `borrowed by '' here`. A pointer is *live* until its last use ([RFC 0006](rfcs/0006-precision.md)). Not reported for a pointer *derived* from `

` (`q = &p->f`, `q = p + 1`): that is a name for the same object, and its later use is a `use-after-free` ([RFC 0011](rfcs/0011-spatial-safety.md)). An error when the loan holds on every path and the release or move happens whenever the call does, otherwise a warning ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.1). RFC 0030 removed `--exclusive-borrows`, the opt-in to RFC 0001's full exclusivity rules. | +| `lifetime-too-short` | error / warning | A pointer may outlive what it points to: `'

' may outlive '', which it points to` (stored into an outer scope, a global or through a parameter) or `returned pointer may outlive '', which it points to`. Notes: where `` is declared and where it goes out of scope. Reported at the store, but decided when `` dies ([RFC 0011](rfcs/0011-spatial-safety.md)): a store undone before then (`ls->fs = fs.prev`), or into a holder that is dead by then, is not reported. `alloca` storage belongs to the frame ([RFC 0030](rfcs/0030-prove-or-trap.md) §8.2), so returning it is reported here too. An error when the escape happens on every path, otherwise a warning ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.4). | +| `unsafe-operation` | error | A raw operation outside a `WEAVEC_UNSAFE` region ([RFC 0004](rfcs/0004-unsafe-boundaries.md)): `dereference of raw pointer '

' outside an unsafe region`, `'' dereferences raw pointer '

' ...` (also `releases`, `takes ownership of`), `raw pointer '

' is assigned to '', which is declared WEAVEC_OWNED, outside an unsafe region` (any safe annotation), `raw pointer is returned from a function whose return type is annotated WEAVEC_OWNED outside an unsafe region`. [RFC 0030](rfcs/0030-prove-or-trap.md) §16 removed the `--strict-externs` forms (`unchecked call to '' outside an unsafe region`, `unchecked call through '' ...`) along with the flag; an unknown callee is now an `unresolved(unknown-callee)` ledger row instead (§5.1). Notes: why the pointer is raw (`'

' is raw: cast from an integer here`, `declared WEAVEC_RAW here`, `loaded through raw pointer '' here`, `handed out by '' here`, each optionally `(through '')`) and `move this operation into a WEAVEC_UNSAFE block or function, or assert the pointer's ownership first`. | +| `mismatched-release` | error / warning | A resource is released (or moved into a consuming parameter) by a function of another release family ([RFC 0007](rfcs/0007-resource-lifecycle.md)): `'

' is released with 'free' but must be released with 'fclose'`. Both names are family names, the canonical releaser of the allocator (`malloc`/`strdup`/`realloc` → `free`, `fopen` → `fclose`, `opendir` → `closedir`, ...), even when the release went through a wrapper defined in the program. Note: `allocated here`. | +| `leak` | warning | An owned resource is lost without being released, moved or stored where the caller can see it ([RFC 0007](rfcs/0007-resource-lifecycle.md)): `'

' is leaked` at the point its last holder goes out of reach (a `return`, a scope end, the statement after its last use); `'

' is leaked: it is overwritten without being released` at the assignment; `'->p' is leaked when '' is freed` (also `'*a' is leaked when 'a' is freed`) at the release of a container whose `WEAVEC_OWNED` field, or a field this function stored an owned value into, still owns something; `result of '' is leaked` at a discarded allocating call. Notes: `allocated here`, `'

' is declared WEAVEC_OWNED here` for a parameter or field, or `reference taken here` for a share retained by a count increment and dropped ([RFC 0010](rfcs/0010-shared-ownership.md); reported only through a *known count*: a field some function in the program releases through, or one annotated `WEAVEC_REFCOUNT`). Not reported: pointers handed to callees the checker cannot follow or cast to integers (they are *escaped*), resources kept by globals or `static` locals when the function returns, blocks that end in a `noreturn` or `exits` call, what is still held at a `return` from `main` ([RFC 0030](rfcs/0030-prove-or-trap.md) §8.4: the process is ending, so it is not a leak), fields of an object this function allocated, and the old block after a failed in-place `realloc`. A warning whatever the certainty ([RFC 0030](rfcs/0030-prove-or-trap.md), *Diagnostics*); `-Werror=weavec-leak` still promotes it. | +| `null-dereference` | error | A pointer that is null on every path reaching here is dereferenced ([RFC 0008](rfcs/0008-pointer-validity.md)): `dereference of '

', which is null`; or passed to a callee whose declaration or library entry requires it non-null: `'

', which is null, is passed to '', which dereferences it` (also `a null pointer is passed to '' ...`). The note says why: `'

' is assigned NULL here`, `'

' is declared WEAVEC_NULLABLE here` / `the result of '' is declared WEAVEC_NULLABLE here`; for a call, also `'' is declared here`. [RFC 0030](rfcs/0030-prove-or-trap.md) §3.2 removed the "may be null" forms: a pointer that may be null has a *checked* null facet (a `nonnull` check in the enforcing modes), and an allocation's result used untested is `allocation-failure` (off by default). | +| `use-of-uninitialized`| error | 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 ([RFC 0008](rfcs/0008-pointer-validity.md)): `use of '

' before it was initialized` (also `'.f'`). Note: `'

' is declared here`. Any assignment, a callee's store (`init(&p)`), a mutable borrow for a call, `memset` or a whole-object write initialises it; `static` and address-taken variables are not tracked. Reported only when it holds on every path ([RFC 0030](rfcs/0030-prove-or-trap.md), *Diagnostics*): a use that is uninitialised on some paths only is defined by zero-initialisation, which the enforcing modes turn on, and produces no diagnostic. | +| `invalid-release` | error / warning | A releaser (or a consuming parameter) is handed a pointer that is not the start of a heap allocation ([RFC 0008](rfcs/0008-pointer-validity.md)): `'

' is released but points to '', which is not a heap object` (a stack or static variable, an array, a field of one; `'' is released but is not a heap object` when `

` is `` itself), `'

' is released but points to a string literal`, `'

' is released but points 4 elements past the start of its allocation` / `points to field 'in' of its allocation` / `does not point to the start of its allocation` (`p + 1`, `strchr(p, c)`, `p++`, `&o->in`; the offset is named when the checker knows it, [RFC 0011](rfcs/0011-spatial-safety.md)). Notes: `'' is declared here` / `allocated here`. When that holds on some paths only, a warning ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.1): `'

' is released but may point to , which is not a heap object`, and for an interior pointer at an unknown offset `'

' is released but may not point to the start of its allocation`. A release the callee may not perform — one it makes only on some result class, under a guard on the arguments, or from a widened case ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.4, §9.1) — makes the finding possible whatever the argument is, which is where the `may be released` forms come from: `a string literal may be released`, `'' may be released but is not a heap object`. | +| `out-of-bounds` | error | An access reaches past the object it is in, or before its start, on every value the facts allow, against an exact extent ([RFC 0011](rfcs/0011-spatial-safety.md); RFC 0030 §3.3: the `may be out of bounds` and `may access past the end` forms of the earlier RFCs are gone — those are *checked* facets now, and produce no diagnostic). Direct accesses: `'

[]' is out of bounds: index of an object of bytes` (both constant; the index is spelled as written, with its folded value in parentheses when that differs), `'

[]' is out of bounds: '' is the number of elements of '

'` / `'' is at least '', the number of elements of '

'` / `'' is above '', ...` (the index related to the count by a condition), `'

[]' is out of bounds: it reaches bytes into '

', which has bytes` (an index the facts pin only through a relation), `'

[]' is out of bounds: index is before the start of '

'` (`it lies before the start of '

'` when no index is named). Library calls with a buffer and a length (`memcpy`, `memmove`, `memset`, `memcmp`, `fgets`, `snprintf`, `read`, `write`, `strncpy`, ...): `'memcpy' accesses 16 bytes of '

', which has 8 bytes` and the relational form `'memset' accesses 'm' bytes of 'p', which has 'n' bytes ('m' is above 'n')`. A callee's requirement at the call: `'put7' requires 8 bytes behind '

', which has 4 bytes`. Three further definite forms ([RFC 0030](rfcs/0030-prove-or-trap.md), *Diagnostics*): `write through '

', which points to a string literal`; `format string of '' reads arguments but are passed`; and `'' copies bytes between overlapping ranges of ''`, note `'' is declared here`. Notes: `'

' is allocated here` / `'

' is declared here` / `the object behind '

' is declared here`. Extents come from allocations (`malloc(n)`, `calloc(n, sz)`, `realloc(p, n)`, and every function in the program that returns one: `xmalloc(n)` returns `fresh extent=n`), from the declared size of a variable, an array or an array member, from string literals, from `WEAVEC_SIZED_BY` on a parameter, and from the count of a sized field ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)), declared or inferred (`'b->data[b->cap]' is out of bounds: 'b->cap' is the number of elements of 'b->data'`, note `'b->data' is declared here`). Strings (RFC 0012): a copy that needs the length plus the terminator is checked like a length (`'strcpy' accesses 6 bytes of 'buf', which has 4 bytes`, `'strcpy' accesses 'strlen(s)' + 1 bytes of 'd', which has 'strlen(s)' bytes` on `malloc(strlen(s))`, `'strcat' accesses 5 bytes of 'buf', which has 4 bytes` counting what `buf` already holds, `'sprintf' accesses at least 5 bytes of 'buf', which has 4 bytes` from the format's minimum), and a terminator-seeking read (`strlen`, `strcpy`'s source, `strcat`'s, `puts`, `printf("%s")`) of an object the checker knows has no terminator (`strncpy` that filled it, `char a[4] = "abcd"`, `memset(a, 'x', sizeof a)`) is `'strlen' reads past the end of 'name', which is not NUL-terminated`, note `'name' is left without a terminator here`. Relations one step further (RFC 0012): `'buf[i]' is out of bounds: 'i' is at least 8 in an object of 8 bytes` under `i >= 8`. RFC 0017 also checks actual converted or wrapped allocation sizes, represented products, VLA dimensions and allocated flexible-array tails; a dimension violation can say `'' is out of bounds for its variable array dimension`, and a caller interval can say `'' requires '

' before its start`. Unresolved indices, unknown sizes or offsets, unsupported field layouts and unknown string lengths do not by themselves produce this error or establish safety. | | `invalid-integer-operation` | error | A definitely invalid supported integer operation ([RFC 0017](rfcs/0017-c-integer-semantics-and-spatial-safety.md)). Message: `invalid integer operation: `, at the source operation. Reasons: `signed integer overflow`, `division by zero`, `signed division overflow`, `invalid shift count`, `invalid signed left shift`, and `nonpositive variable array dimension`. Possibly invalid arithmetic is conservative, without a definite-error claim or using undefined behavior to discard a reachable path. | -| `analysis-incomplete` | warning | An operation could not be modeled completely ([RFC 0014](rfcs/0014-pointer-identity-and-call-effects.md)). Message: `analysis is incomplete: `. Reasons identify unsupported copies of pointer-containing storage, incompatible or unknown object views, unavailable callback contexts, and exhausted function or summary iterations. [RFC 0015](rfcs/0015-array-and-container-ownership.md) adds unresolved array selections/updates, incomplete symbolic composition, unavailable source snapshots, uncertain range membership and element/range limits. [RFC 0016](rfcs/0016-compositional-call-checking.md) adds `unresolved call alias relationship`, `unrepresentable call context input path`, `call context input path limit reached`, `call context relationship limit reached`, and `call context unavailable or limit reached`. [RFC 0017](rfcs/0017-c-integer-semantics-and-spatial-safety.md) adds unsupported numeric widths, expressions, conditions, outputs and extent projections; examples include `unsupported integer width greater than 64 bits`, `unsupported numeric output projection`, `unsupported numeric condition projection`, `unsupported extent requirement condition` and `unrepresentable variable array byte extent`. A represented symbolic array copy can join copied and untouched contents without warning solely because membership is undecided. Known effects still apply; this warning describes missing coverage, rather than proving that the operation itself is invalid. | -| `annotation-mismatch` | error | A definition contradicts its own annotation: `'

' is annotated WEAVEC_BORROWED but is freed here` (also `WEAVEC_MUT`; also `moved`, `written through`; also `... but '

->f' is freed here` for a path under the parameter), `function returns a borrow but its return type is annotated WEAVEC_OWNED`, `function returns a fresh allocation but its return type is annotated WEAVEC_BORROWED` (or `WEAVEC_MUT`). Notes: `'

' is annotated here` / `annotated here`; `'' is a copy of '

'` when through an alias. Callers keep trusting the annotation. A store into a `WEAVEC_SIZED_BY(g)` field of an object smaller than `g` says ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)): `'b->data' is declared WEAVEC_SIZED_BY(cap) but is given 4 bytes where 'b->cap' says 8` (at the store, or at the write to the count when that comes second; `says at least 8` under a lower bound, `says 'n' elements of 4 bytes` for a non-byte element), note `'b->data' is declared here`. An object of unknown size, a larger one, or null is not reported. | -| `annotation-required` | warning | **On by default:** `call to '' is not checked: it has no definition or ownership annotations here`, once per callee per program (RFC 0005: a definition in any unit analysed together with this one counts; alone, the unit is the program), for a callee with pointer parameters or a pointer result that has no body in the program, no annotations and no libc entry; callees from system headers are exempt. Notes: `'' is declared here`, `annotate its pointer parameters with WEAVEC_OWNED, WEAVEC_BORROWED, WEAVEC_MUT or WEAVEC_RAW, or define it in this program`. Likewise `call through '' is not checked: its function type has no ownership annotations and no function of that type has its address taken in this program`, once per function-pointer type. With `--strict-externs` these calls are `unsafe-operation` errors instead (at every call site, including callees from system headers), and their pointer result is raw. **With `--report-unannotated`:** every exported (non-`static`) definition additionally gets `pointer parameter '

' of '' is inferred WEAVEC_OWNED; add the annotation to its declaration` (or `WEAVEC_BORROWED` / `WEAVEC_MUT`; `return value of '' is inferred ...`) with a fix-it that inserts the annotation, or `pointer parameter '

' has no inferable ownership; annotate it with WEAVEC_OWNED, WEAVEC_BORROWED or WEAVEC_MUT` when the body gives no evidence. | -| `invalid-annotation` | warning | A `weavec.*` annotation WeaveC does not recognise, `WEAVEC_NULLABLE` and `WEAVEC_NONNULL` on the same declaration, `WEAVEC_RETAINS` and `WEAVEC_RELEASES` on the same declaration, `WEAVEC_OWNED_BY(f)` without `WEAVEC_OWNED` ([RFC 0010](rfcs/0010-shared-ownership.md)), `WEAVEC_SIZED_BY(n)` on a non-pointer or naming no integer parameter (`'

' is declared WEAVEC_SIZED_BY(n) but is not a pointer` / `... but 'n' is not an integer parameter`, [RFC 0011](rfcs/0011-spatial-safety.md)), `WEAVEC_SIZED_BY(g)` on a field that is not a pointer or whose `g` is no integer field of the record (`field 'data' is declared WEAVEC_SIZED_BY(cap) but 'cap' is not an integer field of 'struct buf'` / `field 'n' is declared WEAVEC_SIZED_BY(cap) but is not a pointer`, once per unit, when the field is first used), or `weavec.assume` on any function but `weavec.h`'s (`'weavec.assume' is not an annotation for 'f'`, [RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)). Reported on definitions. | +| `annotation-mismatch` | error | A definition contradicts its own annotation: `'

' is annotated WEAVEC_BORROWED but is freed here` (also `WEAVEC_MUT`; also `moved`, `written through`; also `... but '

->f' is freed here` for a path under the parameter), `function returns a borrow but its return type is annotated WEAVEC_OWNED`, `function returns a fresh allocation but its return type is annotated WEAVEC_BORROWED` (or `WEAVEC_MUT`). Notes: `'

' is annotated here` / `annotated here`; `'' is a copy of '

'` when through an alias. Callers keep trusting the annotation. A store into a `WEAVEC_SIZED_BY(g)` field of an object smaller than `g` says ([RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)): `'b->data' is declared WEAVEC_SIZED_BY(cap) but is given 4 bytes where 'b->cap' says 8` (at the store, or at the write to the count when that comes second; `says at least 8` under a lower bound, `says 'n' elements of 4 bytes` for a non-byte element), note `'b->data' is declared here`. An object of unknown size, a larger one, or null is not reported. The id also covers *relied-upon* interface facts, and the link step adds two forms of its own ([RFC 0030](rfcs/0030-prove-or-trap.md) §13.2): `'' is declared here but its definition in '' ''`, and `store to '.' breaks '', which '' relies on`. | +| `invalid-annotation` | warning | A `weavec.*` annotation WeaveC does not recognise (including `weavec.checked`, which [RFC 0030](rfcs/0030-prove-or-trap.md) removed), a `WEAVEC_COUNTED_BY(n)`, `WEAVEC_SIZED_BY(n)` or `WEAVEC_ENDED_BY(q)` whose name resolves to no sibling parameter or field or to one of the wrong type (`'n' in WEAVEC_COUNTED_BY does not name a parameter or field`, `'q' in WEAVEC_COUNTED_BY is not an integer parameter or field`, `'n' in WEAVEC_ENDED_BY is not a pointer parameter or field`; the kind is dropped), an extent macro or `WEAVEC_STRING` on a non-pointer (`'x' is declared WEAVEC_COUNTED_BY(n) but is not a pointer`) or on a variable, `WEAVEC_REQUIRE_SAFE` on anything but a function (`WEAVEC_REQUIRE_SAFE on 'x', which is not a function`), two declared kinds of one parameter or field that disagree (`conflicting kinds for 'p': ...`; the weaker is used, [RFC 0030](rfcs/0030-prove-or-trap.md) §7.2), `WEAVEC_NULLABLE` and `WEAVEC_NONNULL` on the same declaration, `WEAVEC_RETAINS` and `WEAVEC_RELEASES` on the same declaration, `WEAVEC_OWNED_BY(f)` without `WEAVEC_OWNED` ([RFC 0010](rfcs/0010-shared-ownership.md)), `WEAVEC_SIZED_BY(n)` on a non-pointer or naming no integer parameter (`'

' is declared WEAVEC_SIZED_BY(n) but is not a pointer` / `... but 'n' is not an integer parameter`, [RFC 0011](rfcs/0011-spatial-safety.md)), `WEAVEC_SIZED_BY(g)` on a field that is not a pointer or whose `g` is no integer field of the record (`field 'data' is declared WEAVEC_SIZED_BY(cap) but 'cap' is not an integer field of 'struct buf'` / `field 'n' is declared WEAVEC_SIZED_BY(cap) but is not a pointer`, once per unit, when the field is first used), or `weavec.assume` on any function but `weavec.h`'s (`'weavec.assume' is not an annotation for 'f'`, [RFC 0012](rfcs/0012-spatial-safety-strings-and-fields.md)). Reported on definitions. | +| `contradicted-assumption` | error | A `WEAVEC_ASSUME(e)` the analysis refutes ([RFC 0030](rfcs/0030-prove-or-trap.md) §6.2): `assumption '' is false here`, with the note `'' is here` at the source of the fact. Minimal trigger: `char b[4] = {0}; int i = 10; WEAVEC_ASSUME(i < 4); return b[i];`. An assumption the analysis neither proves nor refutes becomes a runtime `assert` check in the enforcing modes, and the analysis assumes `e` after it in every case. | +| `allocation-failure` | warning | **Off by default**; `-Wweavec-allocation-failure` (or `-Wweavec`) enables it ([RFC 0030](rfcs/0030-prove-or-trap.md) §3.2, §8.4). The result of an allocating call is used without a null test: `the result of '' is used without a null test; it is null when allocation fails`, note `allocated here`. Minimal trigger: `char *p = malloc(8); p[0] = 1;`. The dereference itself is a checked null facet either way, so in the enforcing modes a failed allocation traps instead of writing through null. | +| `unresolved-operation` | error | Only under `-fweavec-require=checked` or `-fweavec-require=proven` (`--require` in `weavec`), or in a function declared `WEAVEC_REQUIRE_SAFE` ([RFC 0030](rfcs/0030-prove-or-trap.md) §6.3): a facet that is neither proven nor checkable. Message: ` is neither proven nor checkable: []`, for example `access 'b[1000]' is neither proven nor checkable: the extent of 'b' is unknown [unknown-extent]`. `` is `access ''`, `dereference of '

'`, `call to ''`, `release of '

'`, `conversion of '

' to ''` or `boundary of ''`, and the reason is one of the closed list of RFC 0030 §2.3. Minimal trigger: `char *get(void); int f(void) { return get()[1000]; }` with `-fweavec-require=checked`. Trusted facets are allowed at every level. | +| `unchecked-operation` | error | Only under `-fweavec-require=proven` (`--require=proven` in `weavec`; [RFC 0030](rfcs/0030-prove-or-trap.md) §6.3): a facet that relies on a runtime check. Message: ` relies on a runtime