[SwayamInSync]

The 0.2 audit of the public documentation found statements the code or the tests contradict. Each fix below was checked again against the code or a real run before writing it. Where a page now shows a verdict or an error, the example is checked by check-doc-examples.py.

Language reference:

• syntax.rst said C++26 pre/post "belong to the compiler". This Clang implements no C++26 contracts, and with -fverify-contracts a bare pre(...) is an error whose fix-it writes cppverify::pre. A new section shows it with a checked rejects example (the bare contract_assert error included). The README said the same thing ambiguously.
• pointers.rst said a bounded quantifier's bound is "the implicit trigger", and so did ch12, ch14, and ARCHITECTURE. quantify takes patterns only from cppverify::trigger marks, and otherwise the solver chooses its own, as the expressions page already says.
• ghost-proofs.rst called a recursive spec opaque by default. It is unfolded once, and hide is what makes a spec opaque.
• integers.rst said every encoding gives the same verdicts and counterexamples. Every encoding is exact, but one may settle in time what another leaves unresolved, and counterexample values are the solver's choice.
• limitations.rst:
  • recursion is direct and mutual;
  • references also bind to fields and elements of a parameter's buffer (suite/reference_subobject_lowering.cpp);
  • an induction's time follows --collection-timeout over collections;
  • it now defines "fails closed": never a proof, either an error that stops the file or Unresolved with construct.unsupported, and never a counterexample;
  • it lists the forms rejected inside supported code, each with its error and what to write instead: a shadowing local, pointer ++/--, *p = r for a record, and cppverify::aliases across pointee types.
• tooling.rst said run-verify-tests.sh lowers every example first; the public script does not. The row now says what it runs. The page also gives the lit command, with the test tools setup.sh does not build (as the macOS CI job builds them).
• The language index and the book's Part II index said every example is verified; fragments of a larger program are not run.

Front page and case studies:

• index.rst gave build\bin as the Windows output for the Visual Studio generator, which writes build\Release\bin (setup.ps1). The Quick start says where the binaries are in a release archive. The opening names the supported subset.
• The UTF-8 and binary-search pages said their failing tests "fail closed"; those tests fail with checked counterexamples. Their commands now use the options the tests use.

Book:

• ch06 and ch13: hide/reveal apply to the whole function. Revealing can change what a proof reaches, though no setting makes a false claim verify.
• ch07: a swap through a temporary still swaps when the two pointers are equal, so "the swap fails" was wrong. The chapter now shows the contracted swap (verified), the caller's aliasing check, and a swap by sums that fails when both pointers are the same (checked, with its counterexample). The aliasing default covers any pair with one mutable pointer, not only two mutable ones. The text block of bare clauses is gone.
• ch11 links its INT_MIN note to ch18, which explains it.
• ch15: replay also runs on cvc5 and the strict portfolio.
• ch16:
  • a failure to prune the cache is a warning;
  • a Lean fallback result is Certified when Lean checked every obligation;
  • after the strict portfolio it is Proved (portfolio+lean);
  • bare pre(...) is qualified.
• ch17: the first fallback run prints Exported: lean fallback: ... rather than exiting as unresolved. Fallback results can be Certified, and the release gate needs the test tools built.
• ch18 lists every always-on check, including a read after delete and a read of an unwritten local, which were checked with and without --no-check-ub. Shifts follow the C++ standard in use since the C++20 fix.
• ch20: the default jobs are the physical cores or CPPVERIFY_JOBS.
• The book map's Part II is chapters 9 to 20.

Design notes and other files:

• DESIGN:
  • recursion through stores and automatic objects verifies;
  • &x is unsupported because escapes are not modeled (lexical lifetimes are);
  • the cvc5 adapter covers unbounded quantifiers, heap frames, and collections;
  • the Lean fallback also follows the strict portfolio;
  • a schedule line is removed.
• ARCHITECTURE's pipeline names cvc5, portfolio, and race.
• COMPETITIVE:
  • the backends and supported subset in its table;
  • race and trusted contracts among the evidence modes;
  • inductive predicates take no measure;
  • the assessment without the MVP wording.
• REFERENCES drops the project-start schedule and bare construct names.
• REPO_LAYOUT, the design notes index, and UB-CHECKING are corrected.
• The API page and the Doxygen main page list what Transform/ and Backend/ hold.
• third_party/README.md: the Verify tests also run on macOS.
• scripts/coverage-verify.sh wrote its failing input in the keyword syntax, which no longer parses, and || true hid that, so the verification-failure path was never covered. It is qualified now. With pre(false) it would have been vacuous rather than failing, so the input is a plain false postcondition. It now fails with the counterexample result = 1.
• Ten files under samples/ and test/ (from 2026-06) are in the keyword syntax, no longer compile, and are used by nothing. They are removed.

Checked: all 175 documentation examples pass (46 against the verdicts their pages show), and the site builds with sphinx-build -W.