[SwayamInSync]

Plan item A25 (path-level vacuity): the vacuity checks asked only whether anything reaches a verified function's end, its preconditions, its behaviors, and its trusted calls. An assumption that removes some paths and leaves others went unnoticed. That is how F38 verified a false claim without a mark: the contradictory definition of a spec recursive through cppverify::choose made x == 7 impossible, and forty_two verified although forty_two(7) == 0.

On the base

$ cpp-verify paths.cpp
Verified: spec decreases and post: tri
Verified: checked [backend=z3]
Summary: 2 verified in 0.1 s

checked has if (t < 0) return -1; under t == tri(n), which tri's postcondition (result >= 0) makes dead. Nothing says so, and with a wrong fact in that place nothing would.

With this PR

$ cpp-verify paths.cpp
Verified: spec decreases and post: tri
Verified: checked [backend=z3]
paths.cpp:13:3: warning: checked: the facts about tri contradict the path to the true branch here, which the code alone reaches, so every claim on that path holds vacuously; either the path cannot happen, and it is dead code, or a fact about tri is wrong
   13 |   if (t < 0)      // tri's postcondition excludes this
      |   ^
Summary: 2 verified in 0.1 s

The result stays Verified without [vacuous], since the verifier cannot tell dead code from a wrong fact. A cppverify::check(t >= 0); before the branch states the fact in the code and silences the warning.

What it would have caught

F38 itself, reopened: with A19's fix reverted (the call-graph edges through a choose removed, so f below again counts as non-recursive and needs no measure), the base reports Verified: forty_two and nothing else; this PR, on the same reverted converter, points at the branch the bad definition removed:

cppverify::spec int f(int n) { return cppverify::choose(k, n == 7 ? k == f(n) + 1 : k == 0); }

int forty_two(int x)
  cppverify::post(cppverify::result == 42)
{
  cppverify::check(f(x) == f(x));
  if (x == 7)
    return 0;
  return 42;
}

Verified: forty_two [backend=z3]
f38.cpp:7:3: warning: forty_two: the facts about cppverify::choose, f contradict the path to the true branch here, which the code alone reaches, so every claim on that path holds vacuously; either the path cannot happen, and it is dead code, or a fact about cppverify::choose, f is wrong
    7 |   if (x == 7)
      |   ^

With A19 in place, f needs a measure, as main reports.

Design

• Which assumptions. The preconditions, callee contracts, invariants, and checks are the code's own reasoning: a branch they close is defensive code, and the existing rule (dead code alone is not flagged) stays. The facts the verifier adds about specs are different: a spec's postcondition at each application, a cluster's induction hypothesis, a recursive spec's definition, an inductive predicate's unfolding, a reads frame, a choice's axiom. Each is proved before use, so each should be a theorem, and a wrong one is a verifier bug that cuts paths silently. Those are the facts this check withholds: passivization already labels them by origin (spec:, reads:, choose). The builtin specs (validity, a sequence's update and reverse, a constant table) are the language's, so their definitions and facts stay, and a function that applies only them is not checked.
• Specs as free functions. In the second query every other spec is an Uninterpreted copy with its signature and nothing else, so each application is a function of its arguments and no more. Hiding the specs is not enough: the counterexample check holds a model's choices to their axioms, and its refinement gives them back (a branch closed by a choice's axiom went unreported that way).
• Which points. Every trace point a path reaches: a branch taken, a return, a loop's body (the iteration chosen and its condition true), and the path after a loop. For each, a smoke query asks whether all the statements before it refute its guard; only then does a second query, without the spec facts and with every spec hidden, ask whether the code reaches it. The first point found is reported, since the points after it share its cause; a function that applies no spec gets no queries.
• What "reaches" means. The second query's counterexample, certified, or one that needs the value of an opaque spec (counterexample.unchecked), which with the specs' values free is a path of the code. A timeout or unknown reports nothing.
• Loop exit event. The passivizer emitted the loop's exit trace event before the exit assumption, with the guard of the path before the loop, so it could not say whether anything continues after the loop. It is now emitted after the exit assumption with the path that continues; event order, every obligation's trace prefix, and the text of traces are unchanged.
• Bounded, as a warning. A function's points share the time of one smoke query (1 s, or the query timeout when smaller); none starts after it, and the search ends at the first point whose first query is undecided, since every later point's query restates every fact before it. A search cut short omits the warning, as an unsettled vacuity check does.
• Withdrawn with the verdict. Like the other vacuity findings, the warning records its verdict and is dropped when a fixpoint demotes it: a fact that is not established may be the cause.
• Precedent. Dafny's --warn-contradictory-assumptions warns where assumptions contradict a path.

Tests

suite/contradicted_paths.cpp (new): warnings at a branch closed by a spec's postcondition (checked_tri), by a recursive spec's definition (checked_steps), inside a loop (first_negative), at a loop's body (drain), after a loop left only by its return (climb), by a choice's axiom (picked), and by a cluster's induction hypothesis (total_nonneg); none for a branch the precondition closes (defensive, no_spec), one the code reaches (plain), one a cppverify::check states (stated), one closed by a builtin spec's fact or definition (rev_len, rev_empty), or one whose verdict a failed postcondition demotes (uses_wrong). The warnings are checked in order in a stream of their own, with --implicit-check-not=warning:, which does not look inside a span of CHECK-DAG matches; the JSON record carries the warning.

The test's warnings do not appear on the base.

On a release build, the whole Verify suite passes (505 of 506, one unsupported).

Noise. Over all 454 programs of clang/test/Verify, run with this PR, the warning appears in contradicted_paths.cpp alone (its 7 expected warnings): no other test program has a path that the facts about specs close and its code reaches.

Cost. Each of the 184 test programs that apply a spec, verified with this PR and with the check switched off (alternating which runs first, 12 at a time): 1452.8 s against 1428.8 s, 1.7%; without the exhaustive ULEB128 decoder, a stress test lit does not run, within noise (1316.8 s against 1335.4 s). A first version, which checked every point of a function, cost 18% (the decoder took 332 s instead of 90 s), so a function's points now share the time of one vacuity check, no query starts after it, and the search ends at the first point whose query is undecided; the decoder then takes 73.1 s against 65.8 s alone.

Mutants

Each mutant below, applied alone and rebuilt, is run against contradicted_paths.cpp and backend_counterexample_trace.cpp; 11 of 13 are caught:

Mutant	Change	Result
N2	facts of origin spec: stay in the code alone	caught
N3	choices' axioms (origin choose) stay	survives, equivalent below
N4	facts about builtin specs alone are withheld	survives, equivalent below
N5	specs keep their definitions in the code alone	caught
N6	builtin specs are opaque too	caught
N7	no query with every fact first	caught
N8	no query of the code alone	caught
N9	the facts stay in the code alone	caught
N10	reaching needs a certified counterexample	caught
N11	a loop's body without its condition	caught
N12	the loop exit event before the exit assumption	caught
N13	the warning stays when its verdict is demoted	caught
N14	the last point is reported, not the first	caught

• N3: a choice the code applies gets its axiom as a postcondition fact (spec:); a fact of origin choose is the axiom of a choice inside another fact, which is withheld itself, so keeping the axiom alone constrains nothing the code names. It stays classified as a fact about a spec, since it is one.
• N4: a builtin's facts are theorems of its definition, which stays, and the counterexample check evaluates it exactly, so withholding them never lets the code reach a point; keeping them saves the solver the work.
• N8 and N13 survived a first run: the test checked warnings with --implicit-check-not=warning: among CHECK-DAG lines, which does not look between the matches of a group, so an extra warning there passed. The warnings are now checked in a stream of their own.
• A first version also kept facts marked Theorem; every such fact has the origin spec: or reads:, so the test was redundant and is gone.

Docs

• the book, ch16 "When a proof is too easy": the kind of assumption, a worked example (checked by check-doc-examples.py), and how to keep a dead branch;
• tooling: the table of vacuity warnings;
• DESIGN (the vacuity paragraph), ARCHITECTURE (the vacuity checks), release notes.

Not done

• Dafny gets this warning nearly free, from the unsat cores of the proof itself (--warn-contradictory-assumptions); cpp-verify's backends do not extract cores yet, so the check runs queries of its own.
• check-doc-examples.py compares only the first line of a wrapped warning; the rest of this one was compared by hand.