`if ((p != 0) && (p->m))` and `if (p == 0 || p->m)` false-positived: the
walker's encodeConditionWithShortCircuit added the LHS to the Z3 solver for
the RHS encode but never updated the env's non-null marks — and the deref
gate checks `env.isDefinitelyNonNull`, not the solver. So only a fragile
same-line text heuristic (sourceLineShortCircuitProvesNonNull) suppressed the
canonical `p && p->m`; parenthesized / `!=0` forms slipped through.
Fix: in the &&/|| short-circuit handling, extract the LHS null-check
(extractNullCheckedVar) and mark its pointer definitely-non-null for the RHS
encode only, then clear it — short-circuit guarantees the LHS holds when the
RHS runs, and clearing prevents the fact leaking into the else-arm (where the
pointer may be null). Path-sensitive, shape-independent, and the bitwise `&`
case stays flagged (both operands really evaluate).
Drift gate: no per-detector change (null-deref 0.792/0.494/0.609 held) — the
fix removes a real FP class without moving the capped-corpus numbers and is
more robust than the text heuristic it supersedes.
Tests: 3 cases in test_null_deref (parenthesized && safe, || safe, bitwise &
still flagged).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
