read-before-init: 75 of 78 real-world findings are infeasible-path false positives (ADR-0002 FP claim is false)

[hyperpolymath]

Measured on google-flatbuffers-bounty with the M4 build (PR #46): read-before-init produced 78 findings, of which 3 are true positives and 75 are infeasible-path false positives (precision 3/78).

The two false-positive classes (every finding counted)

A. Correlated guards: 71 findings, all in generated Pack methods. Each flagged read has if self.<v> is not None: on the line above; this was checked mechanically for all 71.

if self.name is not None:
    name = builder.CreateString(self.name)
...
if self.name is not None:
    MonsterAddName(builder, name)   # flagged

B. Loops over non-empty literals: 4 findings (tests/py_test.py:153, :183).

for sizePrefix in [True, False]:
    b1 = flatbuffers.Builder(0)
    ...
monster2 = _MONSTER.Monster.GetRootAs(b1.Bytes, b1.Head())   # flagged

The positive control (keep these): python/flatbuffers/flexbuffers.py:1378/1400/1514. A raise in _StartVector() makes the finally read an unbound start, and the resulting UnboundLocalError masks the original exception.

Why this is an ADR problem, not an implementation bug

ADR-0002 (rule 10 counter-conditions) says the rule's only false-positive sources are (a) opacity and (b) scope. Classes A and B are a third source, infeasible paths, and the analysis is path-insensitive by design. PR #46 transcribes the ADR faithfully.

Acceptance criteria

• ADR-0002's rule 10 counter-condition paragraph names infeasible paths as a false-positive source (owner-ruled amendment, as in docs: make PROOF-PROGRESS true, amend ADR-0002 OPAQUE triggers, record D4 #44).
• Class B: a for over a non-empty list/tuple/set/str literal gets no zero-trip exit edge, or the ADR records why not. Add a fixture pair: a negative for the literal loop, and a positive for the same loop over a name.
• Class A: a decision recorded in the ADR on whether to handle correlated guards (e.g. a pruned re-check of an identical pure condition) or accept them. If handled, add a fixture pair and a mutant.
• Re-scan google-flatbuffers-bounty: all 3 flexbuffers findings still reported (the positive control), and the class A/B counts reported against the numbers above.