[SwayamInSync]

A run verified every function of its file, so working on one function meant waiting for all of them and reading past their results. --function=PATTERN now reports only the functions a glob pattern matches (repeatable), with the verdicts a run of the whole file gives:

namespace cv = cppverify;

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

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

int uses_wrong(int x)
  cv::pre(x < 50)
  cv::post(cv::result == x + 1)
{
  int y = wrong(x);
  return y + 1;
}

int uses_add(int x)
  cv::pre(x < 50)
  cv::post(cv::result == x + 2)
{
  int y = add_one(x);
  return y + 1;
}

$ cpp-verify --function=uses_wrong filter.cpp
Unresolved: uses_wrong [backend=z3] [reason=callee.contract] (relies on the contract of wrong, which is not established)
Summary: 1 unresolved (callee.contract 1) in 0.0 s
$ cpp-verify --function=uses_add filter.cpp
Verified: uses_add [backend=z3]
Summary: 1 verified in 0.0 s
$ cpp-verify --function='add_*' filter.cpp
Verified: add_one [backend=z3]
Summary: 1 verified in 0.0 s

On the base (#94) --function is an unknown option.

Stacked on #94. Plan item E5, the filter (the plan's wording: "callees' contracts are used as always, so the selected proofs are the same proofs").

Design

• The same verdicts. A verdict rests on callee contracts, spec facts (definitions, frames, postconditions, unfoldings), and, for a counterexample confirmed by proof, any established lemma. A filtered run must establish what a whole run establishes for the verdicts it reports, or a caller of an unverified callee would be Unresolved where the whole run says Verified, and a caller of a spec whose termination fails would be Verified where it says spec.termination (the second is a wrong proof, since an unrun spec check never marks the spec undefined). So Verifier::run schedules the selected functions, every spec and proof function, and then, round by round, each executable function whose contract the run's verdicts call (CallDependencies, proof blocks' Callees), until none is new. An executable function nothing reported relies on is not verified at all. The fixpoints then run as for the whole file.
• What is printed. A function is selected by the name its verdicts print. An inductive predicate's step prints the predicate's name (spec post by induction failed: climbs), so it is selected with the predicate, and so are the predicate's rule proofs. The diagnostics of functions not selected stay, hidden, for what they establish; so do the errors of functions the verifier does not represent unless selected. The summary counts what is printed, and the exit status follows it (0 when every reported verdict is a proof).
• Patterns are llvm::GlobPatterns over the names verdicts print (Ring::push, total<short>); a pattern that matches nothing is an error. With --list-functions the filter narrows the listing.

Tests

suite/function_filter.cpp (new): the whole file's verdicts; one selected caller of a failing callee (callee.contract, as in the whole run, and only it printed); one of a verifying callee (Verified, so the callee was verified); one using a spec whose termination fails (spec.termination); an inductive predicate with its rules; a predicate whose postcondition fails by induction, a check of its generated step, reported with it; one whose rule proofs stay unresolved (--solver-rlimit=1), reported with it; a glob over two functions with an unsupported function's errors hidden and exit status 0; an archive written by a filtered run, which holds only the selected function and what it relies on; a pattern that matches nothing; and a narrowed listing.

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

Mutant	Change
F1	every function is selected
F2	the callees a verdict relies on are not verified
F3	spec and proof functions run only when selected
F4	what is not selected is printed
F5	the errors of functions not selected are printed
F6	a pattern may match nothing
F7	the listing is not narrowed
F8	a predicate is reported without its rule proofs
F9	the exit status counts what is not reported
F10	a predicate's step is selected by its own name, climbs.step

F8 survived the first run, in which no rule proof failed. F10 is how the first version selected the step, matching the step's predicate by identity where the step records its name: --function=climbs hid the failed induction. The test now has that predicate and one whose rules stay unresolved.

Docs

tooling.rst: --function, its guarantee and exit status. Book ch15, release notes, ARCHITECTURE.md (how a filtered run schedules).

Checked

• lit of clang/test/Verify on E4b: --max-failures, each failure past the failing checks before it #96, which contains this branch: 482 passed, 1 unsupported (darwin only), and 1 failure of E4b: --max-failures, each failure past the failing checks before it #96's own test, which it changed during the run and which passes on the final build.
• On this branch: function_filter.cpp and inductive_rules.cpp pass, and so do docs_examples.test and docs_coverage.test with the new section.