[SwayamInSync]

A run printed its verdicts and stopped, with no total; every spec function that needs no check added a line (Verified: spec axiom: twice) that is not a verdict; there was no way to see only what needs attention, or to list what a run would verify; and --help did not give the default of --timeout. Now:

namespace cv = cppverify;

cv::spec int twice(int x) { return 2 * x; }

int add_one(int x)
  cv::pre(x < 100)
  cv::post(cv::result == x + 1)
{
  return x + 1;
}

int add_two(int x)
  cv::pre(x < 100)
  cv::post(cv::result == twice(x))
{
  return x + 2;
}

$ cpp-verify summary.cpp
Verified: add_one [backend=z3]
summary.cpp:14:23: error: verification failed: add_two [fn_...::postcondition@14:23] (counterexample: result [ssa=__result_1] [type=i32] = 5, x [ssa=x_0] [type=i32] = 3; trace: return.return@16:3 value=5) [backend=z3] [reason=counterexample]
Summary: 1 verified, 1 failed in 0.0 s

$ cpp-verify --quiet summary.cpp
summary.cpp:14:23: error: verification failed: add_two [...]
Summary: 1 verified, 1 failed in 0.0 s

$ cpp-verify --verbose summary.cpp
Verified: spec axiom: twice
Verified: add_one [backend=z3]
summary.cpp:14:23: error: verification failed: add_two [...]
Summary: 1 verified, 1 failed in 0.0 s

$ cpp-verify --list-functions summary.cpp
summary.cpp:3:14: spec twice
summary.cpp:5:5: function add_one
summary.cpp:12:5: function add_two

On the base (#92) the first command prints Verified: spec axiom: twice before add_one and no summary, and the other three are unknown options.

Stacked on #92. Plan item E5, its first half (the filter --function, results printed as they become final, and --time-report follow); decision Q5 taken as recommended: exit codes stay as they are, with the summary.

Design

• The summary counts each verdict as printDiagnostics prints it, into the run's VerifySummary: proofs (Verified, Certified, Proved (z3+lean)), failures, unresolved results with each reason code, bounded-safe, trusted, lowered, exported, interrupted. An error counts only when it carries a verdict, as the first error of a function the verifier does not represent does (construct.unsupported), so a function with two such errors counts once. A verdict the fixpoints demote counts with its new reason; an inductive predicate's line, which had no result of its own, now gets one when demoted, so it counts as unresolved (spec.inductive) and its JSON record has a reason, which it lacked before. The driver prints the counts of every file of the run and the time from its start. JSON output (records are the whole stream), --list-functions, and archive replay (one line per module already) have no summary.
• --quiet leaves out proofs, lowered and exported results, and trusted contracts: what remains is what needs attention, the summary included.
• spec axiom lines come only with --verbose, marked as no verdict, so the summary is the same with or without them.
• --list-functions stops after conversion and prints each function the user wrote with its location and kind (function, spec, constexpr spec, proof, trusted); generated functions (builtins, choices, an inductive predicate's step and rules) are left out, and errors about functions the verifier does not represent are printed as a run prints them.
• --help gives --timeout's default, built from DefaultSolverTimeoutMs.

Tests

• suite/command_line.cpp (new): the summary of a file with each kind of verdict (proofs, a failure, an unsupported function, a trusted contract), --quiet, --verbose (with the same summary), --list-functions (with a function that uses cv::valid, whose builtin spec must not be listed), no summary in JSON, and the default in --help.
• suite/inductive_rules.cpp: the summary and the JSON reason of a predicate whose rules are not established.
• 26 tests that expected spec axiom lines no longer do, and six that pin the end of the output (-NEXT, -NOT: {{.}}) expect the summary; two of them are among the 26.

Each mutant below, applied alone, makes suite/command_line.cpp fail:

Mutant	Change
C1	proofs are not counted
C2	a failure counts as unresolved
C3	an unresolved verdict loses its reason
C4	an error without a verdict counts as unresolved
C5	a spec axiom line counts as a proof
C6	trusted contracts are not counted
Q1	--quiet prints proofs
Q2	--quiet prints trusted contracts
V1	spec axioms are printed without --verbose
L1	generated functions (here cv::valid's builtin spec) are listed
L2	--list-functions verifies too
S1	JSON output gets the summary
S2	--list-functions gets the summary
H1	--help hides the default timeout
C7	a demoted line without a result keeps none (suite/inductive_rules.cpp fails)

Q1, Q2, and V1 survived the first run: the test's -NOT lines stood before -DAG groups, so they checked only the output before the first match. The test now checks the default, quiet, and verbose outputs in order, with --implicit-check-not for what must not appear, which covers every gap between matches.

Docs

• tooling.rst: "What a run prints", with a checked example. Book ch15: the three options.
• release notes, and the examples whose output showed spec axiom lines. ARCHITECTURE.md: how a run counts its verdicts.

Checked

• lit of clang/test/Verify on this branch first: 447 passed, 33 failed, every failure a test that expected spec axiom lines or pinned the end of the output; after the changes above each of the 33 passes. The full run on the branch stacked on this one (E4a) then had no failure of this PR's.
• docs_examples.test and docs_coverage.test pass with the new section and the dropped spec axiom lines.