[SwayamInSync]

A failure printed as one line: the obligation's internal identity, then every SSA version of every variable with its sort, then a trace in internal event names. On abs without its precondition, the base (#99) prints:

abs.cpp:4:3: error: verification failed: abs [fn_5f5a3361627369::overflow@4:3] (counterexample: x [ssa=x_0] [type=i32] = -2147483648; trace: return.return@4:3 value=-2147483648) [backend=z3] [reason=counterexample]

Across the suite such lines had a median of 365 characters (finding F31 of the 0.2 plan). The compiler path was worse: clang++ -fverify-contracts wrote the verifier's text to stderr and then reported one generic cppverify: verification failed error, so -w, -Werror, colors, and -fdiagnostics-format=sarif (which printed "results": []) did not apply to it.

Now a failure is a Clang error at the failing check, and its counterexample and path are notes:

abs.cpp:4:3: error: verification failed: abs [overflow] [backend=z3] [reason=counterexample]
    4 |   return x < 0 ? -x : x;
      |   ^
abs.cpp:4:3: note: counterexample: x = -2147483648

This is plan item E3.

The format

• The error. It names the kind of check ([postcondition], [overflow], ...), not its internal ID; the location already says where the check is. The source line is shown, the failing expression underlined and the caret at its operator, as Clang underlines an expression: ~~~~~~~~~~~^~~~ under cv::result < 3. An expression that runs to another line gets the caret alone. A failure explained by more than its model, such as one confirmed by a proof, keeps its explanation in parentheses.
• The counterexample note. It is placed at the check and lists the values by source name, in declaration order with result last.
  • Each variable appears once, with the values it takes along the path joined by -> (y = 0 -> 1 -> 4).
  • Two variables of one name, a local that hides another, are told apart by their line (i (line 8) = 0 -> 1, i (line 14) = 0 -> 1).
  • A reference is shown as &r = 4, since its value is the address it refers to.
• The path. Each step is a note at its line, in the words of Clang's static analyzer: takes the true branch, enters the loop, starts an arbitrary iteration of the loop, where its condition is true, calls add(9), stores 0 at address 1, creates a local object at address 4, ends the lifetime of a local object, deletes the object at address 4, returns 4. A step the model does not decide reads perhaps ....
  • A path of more than ten steps shows its first and last five, with a note counting the steps left out, as -ftemplate-backtrace-limit does.
  • A step inside a macro is shown where the macro is used. The error already shows Clang's macro backtrace, and each note would repeat it (three expanded from macro 'assert' notes for one assert).
• Other results. Warnings print as Clang warnings; verdicts (Verified: f [backend=z3]) stay one line each, as before.
• JSON. JSON Lines keep every field they had. A record's message is now the error's text: the values and the path stay in model and trace.

Three faithfulness fixes the new format needed

The old line listed what the solver's model held, with SSA names that hinted at how to read it. Printed as a sequence of values, three things in it would have been wrong, so this PR fixes them at their source.

• Values of branches the path does not take. On an untaken branch an SSA version equals the version before it (emitInactiveFrame). Listing every version therefore showed y = 0 -> 1 -> 0 -> 1 -> 4 -> 4 for a y that never returned to 0.
  • Passivization now records, with each version of a source variable, the path condition active where it is defined (PassiveModelVariable::Guard).
  • Lowering carries it as DiagnosticVariable::Guard, the literal true for a version defined on every path. It is a shared, immutable term, validated like a trace guard; simplification drops it if it calls a removed function, which leaves the version's path unknown.
  • Archives record it, as they record trace guards: cppverify.obligation/4 adds it to the diagnostic metadata, never hashed, and reads /3 to /1, whose versions have no guard. A replayed counterexample therefore lists the same values as the source run; one from an older archive lists every version, as before.
  • Z3 evaluates it in the model without completion, as it does trace guards (VerifyModelValue::OnPath). A version whose condition is false is left out of the text, and JSON marks it "on_path": false.
  • A version that keeps the value before it, such as a merge of two branches, adds nothing to the sequence. The same function now reads y = 0 -> 1 -> 4.
• References. A reference variable's value is the address it refers to, which the old line marked [type=pointer]. VSourceVariable::Reference is recorded from the declaration's type and carried to VerifyModelValue::Reference, and the text writes &r = 4, which is what &r evaluates to in C++.
• Steps that do not happen. A store, a delete, and a return emitted their trace event before the checks of their own operation. So a failing overflow check in return -x; listed return.return@12:3 value=-2147483648, the wrapped value, and one in r = r + 1; listed heap-write.store@6:5 address=4 value=-2147483648.
  • The events now come after those checks, so a check that fails at the operation ends the path before it (in JSON as well).
  • A call keeps its event before its precondition, which is checked as the call happens.

Ranges

To underline the whole expression, every VExpr now carries the start of its source (BeginLoc, Clang's getBeginLoc) beside Loc (getExprLoc, the operator) and EndLoc. Every copy of EndLoc in conversion, passivization, spec inlining, lowering, simplification, induction, and the Z3 and cvc5 adapters copies BeginLoc too. The result is VerifyResult::BeginLocation. Before, the range ran from the caret: cv::result >= 0 && cv::result <= 100 was underlined from &&, which suggested that only the right conjunct had failed.

The compiler

-fverify-contracts reports every result through the compiler's DiagnosticsEngine. The verifier's thread collects VerifyDiagnosticParts (VerifyOptions::Parts) instead of printing them, and finishCppVerify reports them on the main thread, which the engine requires:

Result	Diagnostic
failure, unresolved, interrupted	err_cppverify_result
warning	warn_cppverify_result, in -Wcppverify
proof	remark_cppverify_result, in -Rcppverify, at the function's declaration
each note	note_cppverify_result

So -Wno-cppverify, -Werror=cppverify, -w, colors, and SARIF apply, and clangd can show them. err_fe_cppverify_failed remains only for a run that fails without a result of its own. DIAG_SIZE_FRONTEND grows from 200 to 250 for the four diagnostics.

$ clang++ -std=c++17 -fverify-contracts -Rcppverify -c summary.cpp -o summary.o
summary.cpp:5:5: remark: Verified: add_one [backend=z3] [-Rcppverify]
    5 | int add_one(int x)
      |     ^
summary.cpp:14:23: error: verification failed: add_two [postcondition] [backend=z3] [reason=counterexample]
   14 |   cv::post(cv::result == twice(x))
      |            ~~~~~~~~~~~^~~~~~~~~~~
summary.cpp:14:23: note: counterexample: x = 3, result = 5
summary.cpp:16:3: note: returns 5
   16 |   return x + 2;
      |   ^
1 error generated.

Where the design comes from

• Clang's own diagnostics: TextDiagnostic for the error, the caret at the operator inside the expression's range, notes, macro expansion notes, -ftemplate-backtrace-limit for long paths.
• The static analyzer's path notes for the trace.
• Verus and Dafny, which report a failed assertion as an error at its span, with related locations as notes.

Tests

• clang/test/Verify/compile_diagnostics.cpp (new): the compiler path, covering the error with its range and notes, -Rcppverify remarks at their functions, the -Wcppverify warning under -Wno-cppverify and -Werror=cppverify, an unresolved result as an error, the error count, SARIF results with their rule IDs, and -fno-verify.
• clang/test/Verify/suite/failure_notes.cpp (new), under --strict-whitespace, so the underline's columns are checked:
  • every kind of path step;
  • values along the path, with an untaken branch left out;
  • &r;
  • the long-path elision;
  • the caret alone for a two-line expression;
  • a macro;
  • no step for a return or a store whose own check fails;
  • JSON on_path;
  • BMC's numbered iterations.
• 110 existing tests that expected the old line now expect the error and its notes, converted by script and then by hand, with values checked against the verifier's output. contracts_link_check.test expects the proofs of a compilation as remarks at their functions.
• obligation_archive.test replays a record of schema v3 and rejects an invalid guard flag; its Python helper reads schema v4 and writes v3.

The documentation's failures were regenerated from the verifier's output: 61 failures on 14 pages and the README. The prose that explains the format was rewritten in the reference (commands and flags, functions and loops) and the book (chapters 12 and 16), with entries in the release notes, docs/ARCHITECTURE.md, and docs/DESIGN.md. website/scripts/check-doc-examples.py passes on the pages (261 examples checked, 105 against the verdicts their pages show, 0 failed).

The whole Verify suite passes on a release build: 490 tests, 1 unsupported (1396 s at 48 workers).

On the base (#99), compile_diagnostics.cpp and failure_notes.cpp fail from their first check: the compiler has no -Wcppverify group, reports one generic error, and every failure is the one-line format.

Each mutant below, applied alone and rebuilt, is caught by compile_diagnostics.cpp, failure_notes.cpp, local_names.cpp, or inductive_counterexamples.cpp (31 of 31):

Mutant	Change
C1	versions of untaken branches are listed
C2	a version that keeps the value before it is listed again
C3	two variables of one name lose their lines
C4	a reference prints without &
C5	result is not listed last
C6	versions are listed in model order
C7	a branch step loses its direction
C8	the loop-iteration step has other words
C9	an undecided step is not marked perhaps
V1	the underline starts at the caret
V2	an expression that runs to another line is underlined
V3	a long path is not shortened
V4	a note inside a macro keeps the macro's location
V5	the counterexample note has no location
V6	an unresolved result is a remark
V7	a proof remark has no location
V8	JSON drops on_path
V9	failures get no counterexample or path notes
I1	the compiler adds its generic error to every failing run
I2	warnings are reported as errors
I3	the underline is dropped in a compilation
P1	versions get no path condition
P2	a return is traced before its value's checks
P3	a store is traced before its checks
O1	path conditions are not lowered
O2	obligations keep no begin location
S1	archives drop the path conditions
Z1	Z3 never evaluates a version's path condition
Z2	Z3's values lose the reference flag
A1	expressions begin at their caret
A2	references are not recorded

Stacked on #99.

Also: two test budgets

confirmation_invariants.cpp (from #97) and extent_separation.cpp timed out on macOS runners in the last round (#95, #97, #98), each looking for a failure the solver finds locally in 0.4 s and 1.7 s. Run 24 at a time beside each other here, they took up to 3.1 s and 4.9 s, against budgets of 5 s and 30 s; the runners' slower cores cross them. Their runs now get 20 s and 120 s. confirmation_invariants.cpp still checks that the confirmation stops in under a second, which is what it is about.