Fix analyzer exit proofs across catches, finally blocks, and local jumps

[thomhurst]

Fixes #833.

RESP001 disposal and RESP002 pending-read proofs share an exception-aware control-flow traversal. Local jumps, correlated catch filters, and loop exits are accepted when every relevant path reaches cleanup; bypass paths still warn.

• Replace duplicated lexical conditional/switch exit heuristics with graph queries from the actual acquisition or pending origin.
• Track branch selection through catches, filters, finally continuations, and iterator disposal. Distinguish exact exception constructions, nullable thrown values, generic constraints, and rethrows. Opaque calls and properties, including branch conditions, can enter local handlers before proof barriers. Explicit casts retain their possible evaluation exceptions; catch origins retain enclosing branch predicates.
• Invalidate predicate evidence at traversed writes. Writes before selection or after cleanup preserve valid correlation. Normalize complementary Boolean predicates and distinguish address-taken locals from array-index expressions.
• Bound queries to fewer than 16,384 processed states and 64 path facts, honor cancellation, and document conservative limits in docs/ANALYZER_LIMITS.md. Barrier failures and uncaught implicit exceptions remain outside the intraprocedural proof.

Integrated main's newer exception regression suite. Updated expectations only for paths now proven safe: local jumps, correlated filters, and nullable values whose possible exception types all reach a flush. Unsafe counterparts remain covered. Allocation-failure paths now warn when their handlers bypass cleanup. ProcessedStateLimitRetainsWarning and PredicateLimitRetainsWarning exercise both search limits with safe and unsafe counterparts.

Validation: all 1343 analyzer tests pass; analyzer and test projects build with zero warnings and errors.

Review follow-up: SearchState is a named readonly struct implementing IEquatable, shared by the pending stack and earliest-entry map. CorrelationRequiresStableEquivalentValues covers ref/out calls, captured lambda mutations, and compound assignments between selection and cleanup for both analyzers. Implicit operation failures now live in ImplicitExceptionClassifier, separate from graph traversal and catch dispatch. Barrier-resolution extraction and a shared operation index remain optional follow-ups; no analyzer allocation-performance claim is made. The diagnostic-limit behavior is documented without changing diagnostic messages. ReservePathFlag exhaustion returns 0: wrapped transfers omit the unproven barrier, and type-initialization facts require a nonzero flag before suppressing an exception edge. Captured-receiver facts also reject UnknownPathFlag. All callers therefore remain conservative.

Return-transfer regression coverage: TupleReturnWithThrowingSecondElementRetainsWarning contains the literal tuple return and bare catch requested by review, with RESP001 asserted. TupleReturnWaitsForAllElements includes a throwing later tuple element with an empty matching catch (RESP001 required), cleanup in that catch (no warning), safe returns, and conditional selection. ReturnConversionPrecedesOwnershipTransfer also covers boxing allocation failure before ownership leaves the method.

Static-call review clarification: responsibility transfers at callee entry; exceptions inside an ownership-taking method or setter remain outside the intraprocedural contract, like disposal/flush failures. Type initialization is checked before entry. StaticMemberBodyCanBypassCleanup explicitly covers a successful static constructor followed by a throwing static method, getter, or setter before cleanup, for both RESP001 and RESP002. Those ordinary calls still retain opaque exception paths. This boundary is documented in docs/ANALYZER_LIMITS.md.

Local-initializer review: ownership now transfers after the complete initializer, including tuple elements and implicit boxing/user-defined conversions. LocalInitializerCompletesBeforeTransfer covers failing and safe cases. Deconstruction-order review: retained target-location evaluation before RHS evaluation, as specified in Roslyn evaluation order. DeconstructionEvaluatesIndexBeforeRhsAtRuntime confirms the actual execution order; DeconstructionTargetExceptionsPrecedeRhsWrites preserves the warning for the supplied example and accepts unconditional catch cleanup.

Tuple-local deconstruction regression: TupleAndFrameworkOperationsUsePreciseFailures includes var pair = (1, 2); int a, b; followed by (a, b) = pair; inside a try/catch before cleanup. It asserts no diagnostic for both RESP001 and RESP002. The same theory covers a nested tuple local, a throwing property target, and boxing conversions that must still warn. These cases passed in the full 877-test run on this commit.
Transfer-flag exhaustion review: TransferFlagLimitRetainsWarning directly exercises the FindBarrierLocation zero-flag branch with 65 distinct owner references in switch arms (each reserves a transfer flag before traversal). The safe 2-arm control has no diagnostic; the safe 65-arm case conservatively warns; a throwing later argument warns at both sizes. Barriers stop traversal paths. Omitting a barrier therefore adds reachable paths and cannot turn a real bypass into a proof of safety. All four cases pass in the 916-test run. A comment at the sentinel return records this invariant.

Summary by CodeRabbit

• Bug Fixes
  • Refined resource-disposal and pending-read diagnostics to account for reachable paths, applicable exception handlers and filters, finalizers, and local jumps.
  • Checks each awaited pooled-result acquisition individually, including those in assignments and initializers.
  • Recognizes flushes through aliases and stored completion tasks, and reports a pending-read warning only when a qualifying flush is not guaranteed on every path.
  • Improved handling of exception types, null conditions, reassigned references, and uncertain analysis outcomes when determining whether warnings apply.
• Documentation
  • Added guidance on analysis behavior, limitations, cancellation, and caching.

Classifier review follow-up: extracted 21 operation-classification methods and their per-query cache into ImplicitExceptionClassifier, with SemanticModel, FlowConditions, and cancellation dependencies. The classifier neither walks graph paths nor dispatches catches. Verified moved method bodies are unchanged apart from visibility and dependency naming; all 1343 analyzer tests pass after extraction. FlowConditions.UnknownPathFlag names exhausted capacity, and non-null/type-initialization guards explicitly reject it. The predicate cap now derives from the ulong width. Documentation explicitly states that duplicate stack entries count toward the state budget, preserving conservative existing behavior.
Design review acknowledgment (1053e9e): further barrier/dispatch extraction, a spilling bitset or limit telemetry, and exact-local-type caching/shared write analysis are deferred follow-ups. The current bounded analysis is intentional: larger state representations and cache lifetime changes need separate performance and invalidation validation, and no performance improvement is claimed here. The exception classifier extraction is complete. The exact-constructor allowlist already has an explanatory comment in ScopeExitAnalysis: only the audited framework constructors that store their supplied message/inner exception receive this precision; constructors outside that list, including ArgumentNullException, remain conservatively opaque rather than being declared unsafe. A before/after corpus comparison has not been performed; validation reported here is the 959-test analyzer suite and project builds, with repository CI still pending. All paginated review threads were checked and resolved as of this acknowledgment; new findings will continue to be checked.
Return/finally review: a returning owner now traverses its finalizers before the successful transfer continuation ends. Explicit and implicit finalizer failures that reach local handlers retain cleanup obligations. ReturnTransfersAfterFinallyCompletes covers leaking and cleaned-up handlers, a safe finalizer, and disposal before a finalizer throws. Array-store review: the supplied fresh-array store already follows typed null/bounds/covariance dispatch on the pre-fix head; ArrayTransferUsesSpecificFailures pins its no-warning result for an unrelated InvalidOperationException catch plus three unsafe null/bounds/covariance controls. No exception-classification change was needed for that finding.
Latest review fixes: anonymous-object member references now wait for the complete construction and any enclosing transfer; later member evaluation and allocation failures retain cleanup obligations. Static member body exceptions preserve successful type initialization, while initializer and constructor-allocation failures keep their separate paths. Checked arithmetic retains the ranges of promoted byte, sbyte, short, ushort, and char operands, including nullable operands; overflowing multiplication and narrowing compound assignments still warn. The 27 added regression cases cover safe and unsafe counterparts, and all 1343 analyzer tests pass with a zero-warning project build.
Await and conversion review fixes: awaited flush barriers now include argument evaluation and completion-adapter arguments before the barrier. Flush/await body failures retain the documented exclusion. AwaitedFlushWaitsForArguments covers throwing cancellation-token and ConfigureAwait arguments, Task.WhenAll arguments, safe calls, and catch cleanup. Direct default ValueTask and ValueTask awaits no longer gain invented exception paths; unknown values retain them. Built-in as conversions now participate in enclosing transfer boundaries, so later argument failures retain disposal obligations. The 17 added cases pass in the complete 1036-test analyzer suite; project builds report zero warnings and errors.
Null-value review fixes: reference-array stores of null no longer gain an ArrayTypeMismatchException path, including deconstruction stores. Null-receiver and bounds failures remain modeled. Boxing a nullable value proven empty by a stable branch no longer gains an allocation failure; subsequent writes invalidate the proof, and unknown or nonempty values remain allocation-capable. FlowConditions.IsKnownNull uses the existing bounded predicates and does not re-read captured locals after writes. Eleven added cases pass for RESP001 and RESP002; all 1343 analyzer tests pass and project builds have zero warnings and errors.
Checked and nullable review fixes: checked/unchecked expression wrappers now reach the enclosing ownership-transfer boundary, preserving failures in later arguments. Nullable.HasValue conditions, including Boolean equality and negation, constrain the same null predicate as null patterns; writes still invalidate those facts. A proven-null throw dispatches only NullReferenceException rather than also entering handlers for the declared exception type. Fifteen new regression cases include unsafe writes, unknown values, and catch cleanup. All 1062 analyzer tests pass; analyzer and test projects build with zero warnings and errors.
Decimal-negation review verification: the reported overflow premise is incorrect. Decimal has symmetric minimum and maximum magnitudes (Microsoft documentation). DecimalNegationHasSymmetricRange executes both ordinary and checked negation of decimal.MinValue and verifies decimal.MaxValue; it also verifies the reverse boundary. ArithmeticUsesSpecificExceptionTypes now pins no-warning results for ordinary, checked, unchecked, and nullable decimal negation in both analyzers, plus an overflowing decimal multiplication control. All six added cases pass without changing analyzer logic; the full 1068-test suite passes and project builds have zero warnings and errors.
Limit-safety verification for the c9c1549 design review: ReservePathFlag checks capacity before shifting and returns UnknownPathFlag (0) at 64 facts. FindBarrierLocation rejects that sentinel before OR-ing _transferFlags, omitting the unproven barrier. TransferFlagLimitRetainsWarning directly tests 65 transfer references with safe and unsafe counterparts.

Search returns true for a possible path, including budget exhaustion; it never means all paths reach cleanup. CollectivelyPostDominates rejects a possible reacquisition bypass and negates the exit-bypass query. RESP002 completion proof likewise requires !CanReachWithoutCrossing, so exhaustion cannot prove a flush. Definition queries retain additional possible definitions and require all of them to match; they do not drop uncertain definitions. The Search exhaustion comment and ANALYZER_LIMITS.md already state this conservative direction. These checks and all three limit regression groups are included in the passing 1068-test suite. No behavior change is needed for these two concerns.
Guarded arithmetic and cast review fixes: division, remainder, and compound division consult tracked nonzero predicates before dispatching DivideByZeroException. Successful type tests suppress InvalidCastException only for an identity or implicit reference conversion from the proven type; numeric conversions do not prove compatible unboxing. Facts remain bounded, writes invalidate them, and captured operands are not re-read through current local facts. Fifteen added cases exercise both analyzers, including overwritten guards, unknown values, incompatible boxed numeric types, an interface cast, and a genuine overflow path. All 1083 analyzer tests pass; project builds report zero warnings and errors.
Default-await precedence review: the reported false negative does not reproduce. The C# or-pattern is part of the is-expression, and the following && type check already applies to both alternatives. Added default(Task) and default(Task) regressions with a NullReferenceException catch; both RESP001 and RESP002 warnings were present before any classifier edit. Explicit parentheses now make that existing grouping easier to read. All seven default-await cases and the full 1085-test analyzer suite pass; project builds report zero warnings and errors.
Latest review fix: casts whose operands are proven null no longer dispatch an impossible InvalidCastException. Reference casts and nullable unboxing accept null; non-nullable unboxing still dispatches NullReferenceException. Nine regression cases cover both analyzers, null guards, nullable and non-nullable destinations, overwritten operands, and unknown operands. Four cases reproduced false warnings before the fix. All 1094 analyzer tests pass, and the analyzer test project builds with zero warnings or errors.
Latest ownership-boundary fixes: instance method groups now transfer only after delegate creation completes, including explicit delegate construction. Executed coalescing assignments use the assignment boundary, and assignment boundaries include the final RHS conversion while preserving pre-store checks and excluding the accepting setter body. Fifteen regression cases cover method-group allocation, boxing in simple and coalescing assignments, catch cleanup, target failures, and skipped coalescing assignments. The explicit delegate constructor and null-guarded coalescing assignment reproduced missed warnings before these fixes. All 1109 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest review fix: ownership-bearing member initializers now propagate through the enclosing object or with expression to its destination. Later initializers and later call arguments can therefore reach local handlers before ownership transfers. Ten regression cases cover ordinary and target-typed construction, local and assignment destinations, with expressions, later arguments, and catch cleanup. Five cases reproduced missed diagnostics before the fix. All 1119 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest Greptile fix: standalone object creation with an ownership-bearing initializer now uses the completed expression statement as its transfer boundary. This includes all member initializers, including conditional initializers lowered into later CFG blocks, instead of stopping at the constructor closing parenthesis. Five regression cases cover throwing and safe initializers, catch cleanup, and conditional initializers. The reported case reproduced a missed warning before the fix. All 1124 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest review fixes: tuple equality now accounts for user-defined element equality operators, including nested tuples, tuple variables, and lifted nullable elements, while primitive, string, and ordinary reference equality remain non-throwing. Synchronous framework GetAwaiter/GetResult completion chains now register the same flush/adapter exemption as awaited completion; argument evaluation still dispatches failures. Sixteen regression cases cover both behaviors. Three missed tuple diagnostics and three false synchronous-flush diagnostics reproduced before the fixes. All 1140 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest review fixes: object-initializer property setters retain their callee-entry ownership boundary, while field stores still wait for completed construction. Collection-element transfers include the complete argument conversion before implicit Add entry; Add-body failures remain excluded. Assignment facts now snapshot known null/non-null RHS values before target invalidation, including constants, guarded aliases, and self-copies. Relevant assignment sources are collected through a worklist so earlier aliases retain needed facts. Fourteen additional cases cover these paths. A prior conservative conditional-throw expectation is now proven safe; its inverted unsafe counterpart still warns. All 1154 analyzer tests pass, and the analyzer test project builds with zero warnings or errors.
Latest review fix: captured lambdas and method groups now enter the normal enclosing-transfer analysis after delegate creation instead of ending the proof there. Ownership waits for the accepting call or initializer, and a delegate-creation trigger preserves conditional-path evidence. Six regression cases cover later argument failures, explicit delegate construction, method groups, anonymous initializers, safe calls, and catch cleanup. Four cases reproduced missed warnings before the fix. All 1160 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest review fix: implicit expanded params arrays are checked for allocation failure before callee entry even though Roslyn assigns them the whole call span. Completion exemptions apply only to invocation/await operations, so Task.WhenAll parameter-array allocation remains visible. RESP002 now combines batch escape and flush barriers in one proof, accepting normal-path transfer plus catch-path flushing while retaining warnings for uncovered paths. Validation also reproduced and fixed a delegate-creation trigger missing across conditional arguments. Thirteen additional regression cases cover these behaviors. All 1173 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest Greptile fixes: batch escape candidates now exclude inspection-only uses such as null comparisons, patterns, ordinary receiver reads, and object equality checks, including transparent conversions. Both individual and collective batch-transfer proofs reject candidates reachable after reassignment since the pending origin, so transferring a replacement batch cannot satisfy the original pending read. Nine regression cases cover inspections, conditional and unconditional replacement, valid original transfers, and flushing before replacement. Seven cases reproduced missed warnings before the fixes. All 1182 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest arithmetic review fixes: signed division/remainder overflow now requires a dividend capable of reaching the signed minimum as well as a possible -1 divisor. Existing small-operand ranges and constant dividends exclude impossible overflow, while checked narrowing and native-integer widths remain conservative. Lifted arithmetic with a proven empty operand skips underlying operator failures, while operand evaluation still runs and can throw. Relevant lifted operands retain earlier null guards. Nineteen regression cases cover safe promotions, unsafe signed division, nullable binary/unary/compound/increment operations, reassignment, and throwing operand evaluation. Fourteen cases reproduced false warnings before the fixes. All 1201 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest Greptile fix: declaration-pattern aliases are followed to their actual escape uses instead of being discarded as inspections. Binding an alias alone does not satisfy the pending obligation, and alias reassignment still invalidates transfer candidates. Alias chains are cycle-guarded, and unconditional var patterns constrain the flow to their matching branch. Eight regression cases cover direct/chained aliases, inspection-only binding, replacement of either local, conditional transfer, and mixed flush/transfer paths. Five cases reproduced false warnings before the fix. All 1209 analyzer tests pass; the analyzer test project builds with zero warnings or errors.
Latest review fixes: pattern aliases now check reassignment from their binding, including replacements before pending creation and chained aliases. Six regression cases cover replaced aliases and preserved copies. Thrown-local type analysis now passes cancellation through syntax and semantic queries, reuses cancellable reference lookup, and caches results (including unknown types) per local within each traversal. All 1215 analyzer tests pass; the analyzer test project builds with zero warnings and errors.
Further review fixes: checked unary negation uses the promoted operand range; null lifted arithmetic no longer hides property stores; captured compound-assignment property targets retain setter failures after pending creation. Pattern alias traversal now includes recursive patterns and direct or stored flush completion, ignores nullable annotations when identifying batch types, and retains reassignment checks from each binding. Added 23 cases, including helper transfers, replaced aliases, partial flush paths, and setter cleanup. All 1238 analyzer tests pass; build reports zero warnings and errors.
Compound-operator review fix: overloaded compound assignments now transfer ownership only after RHS evaluation and operator type initialization. The operator body remains outside the ownership-transfer proof, matching binary and unary operators. Six regression cases exercise both analyzers, including later throwing tuple elements, conditional operands, catch cleanup, and static initialization. All 1244 analyzer tests pass; build reports zero warnings and errors. The latest Claude suggestions about barrier/dispatch extraction and an operation index remain deferred as described above; transfer-flag exhaustion is already covered by TransferFlagLimitRetainsWarning and the linked conservative-limit explanation.
Nullable-conversion review fix: known-null numeric operands no longer create an OverflowException edge. Lifted conversions return null; non-nullable conversions still retain their InvalidOperationException edge from unwrapping. Seven regression cases cover decimal, floating-point, and checked integral conversions, unknown and overwritten values, and non-nullable destinations for both analyzers. Four cases reproduced false warnings before the fix. All 1251 analyzer tests pass; build reports zero warnings and errors.
Documentation review clarification for 98cfe85: the cited symbols exist at this head. ReachabilityWalker is a private nested class, with MaxProcessedStates at line 23; FlowConditions.MaxPredicates is also the exact current name. ANALYZER_LIMITS.md describes implementation limits, not public APIs, so private visibility does not invalidate these references. No naming change is needed. The cancelled integration reports belong to superseded heads; current-head CI remains in progress, and the local 1251-test analyzer run and build are green. Barrier/dispatch extraction and a PathFacts abstraction remain follow-up refactoring, rather than changes to the bounded proof contract in this PR.
Range-guard review fix: nonzero evidence now checks whether zero contradicts a known numeric comparison, rather than requiring the comparison constant itself to be zero. This covers positive and negative ranges and equality to nonzero constants while retaining warnings for ranges containing zero and overwritten guards. Eleven added cases exercise both analyzers; six reproduced false warnings before the fix. All 1262 analyzer tests pass; build reports zero warnings and errors.
Event-capture review fix: removing a captured delegate from an event no longer counts as transferring ownership. Event addition transfers at add-accessor entry, after delegate allocation, receiver validation, and static event type initialization. Eight regression cases cover method groups, lambdas, explicit delegate construction, add-accessor body exceptions, and pre-entry failures with a cleanup counterpart. Four cases reproduced incorrect diagnostics before the fix. All 1270 analyzer tests pass; build reports zero warnings and errors.
Latest review fixes: anonymous objects assigned to discards now use the constructor boundary, preserving allocation and initializer failures while accepting successful construction and catch cleanup. The reported unsafe case already warned; added controls reproduced false warnings for safe construction. RESP002 completion candidates are no longer filtered by lexical position. Target reachability compares operation order inside a CFG block, since Roslyn can merge forward-goto destinations in execution order despite reversed source offsets. Ten added cases cover these behaviors, including missing flush branches, replaced batches, aliases, and mixed transfer/flush paths. All 1280 analyzer tests pass; build reports zero warnings and errors.
Unsigned-compound-division review clarification: the supplied byte value; checked { value /= -1; } example is rejected by C# with CS0031, rather than executing a narrowing conversion. Six compiler regression cases pin CS0031 for byte/ushort negative operands and CS0266 for the related char/uint forms. Three analyzer cases verify valid unsigned division does not acquire an impossible OverflowException edge. No classifier change is warranted for this finding. All 1289 analyzer tests pass; build reports zero warnings and errors.
Compound-shift review fix: checked left-shift assignments to narrow integral targets now retain OverflowException from the non-identity output conversion. This is distinct from the shift itself, which does not overflow; see the C# compound-assignment specification. A runtime test confirms that a byte containing 128 throws when shifted left by one in a checked compound assignment. Twelve analyzer cases cover signed and unsigned small types, nullable targets, unchecked and full-width shifts, right shifts, and zero effective shift counts. All 1302 analyzer tests pass; build reports zero warnings and errors.
Signed-remainder review clarification: removing the overflow edge would be incorrect. The C# remainder specification explicitly requires OverflowException for the signed minimum and -1 when the corresponding division throws. Three no-inline runtime tests confirm this for int, long, and nint on the current runtime. Six analyzer cases preserve these exception paths, including checked and unchecked forms and a safe positive-divisor control. No classifier change is needed. All 1311 analyzer tests pass; build reports zero warnings and errors.
Built-in delegate combination and removal now preserve allocation failure paths for RESP001 and RESP002, including compound assignment. Regression tests cover both operators, catch cleanup, unrelated catch types, and incompatible runtime delegate types. All 1321 analyzer tests pass; the changed projects build without warnings or errors.
Delegate combinations now use known-null operand facts, including preceding assignments, to omit impossible allocation and incompatible-type failures. Non-variant delegate types also exclude incompatible runtime-type failures. Twelve additional regression cases cover these proofs and retain allocation warnings for unknown non-variant operands. All 1333 analyzer tests pass; the changed projects build without warnings or errors.
The checked bitwise narrowing review example is rejected by C# with CS0266: an int variable cannot be used as the right operand of byte |= in that example. Five compiler regression cases verify rejection for |=, ^=, &=, unchecked, and nullable variants. Five valid same-type bitwise cases verify that neither analyzer invents an overflow path. No classifier change was needed. All 1343 analyzer tests pass; the changed projects build without warnings or errors.

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 22 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: 81a5d3d0-a540-406f-a52b-79260a54d5ca

📥 Commits

Reviewing files that changed from the base of the PR and between 4bd1b16 and 0c776f2.

📒 Files selected for processing (4)

• src/Respire.Analyzers/FlowConditions.cs
• src/Respire.Analyzers/ImplicitExceptionClassifier.cs
• src/Respire.Analyzers/ScopeWalker.Traversal.cs
• tests/Respire.Analyzers.Tests/ExceptionAwareFlowTests.cs

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: a7d8d4b8-b77e-4b24-92b7-ba2dd7d19ad6

📥 Commits

Reviewing files that changed from the base of the PR and between 60907c2 and 4bd1b16.

📒 Files selected for processing (6)

• src/Respire.Analyzers/FlowConditions.cs
• src/Respire.Analyzers/ImplicitExceptionClassifier.cs
• src/Respire.Analyzers/PendingReadBeforeFlushAnalyzer.cs
• src/Respire.Analyzers/ScopeExitAnalysis.cs
• src/Respire.Analyzers/ScopeWalker.Traversal.cs
• tests/Respire.Analyzers.Tests/ExceptionAwareFlowTests.cs

Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.

---

📝 Walkthrough

Walkthrough

The analyzers now use bounded, exception-aware control-flow searches to evaluate reachability and transfer barriers. RESP001 checks acquisitions individually, and RESP002 evaluates escape uses and flush completions. Tests and documentation cover handler behavior, path evidence, and analysis limits.

Changes

Analyzer Control-Flow Proofs

Layer / File(s)	Summary
Path and exception evidence src/Respire.Analyzers/FlowConditions.cs, src/Respire.Analyzers/ImplicitExceptionClassifier.cs, src/Respire.Analyzers/ScopeExitAnalysis.cs	FlowConditions tracks bounded branch predicates and receiver facts. ImplicitExceptionClassifier classifies potential implicit exceptions. ScopeExitAnalysis provides cancellation-aware exception-type evidence and no longer contains intra-scope exit and catch-dispatch analysis.
Reachability queries and barriers src/Respire.Analyzers/ScopeWalker.cs, src/Respire.Analyzers/ScopeWalker.Traversal.cs	ScopeWalker uses bounded path searches for reachability and barrier queries. The search tracks transfers, iterator disposal, implicit exceptions, exception dispatch, and paths through finally regions.
Analyzer disposal and flush checks src/Respire.Analyzers/UndisposedPooledResultAnalyzer.cs, src/Respire.Analyzers/PendingReadBeforeFlushAnalyzer.cs	RESP001 checks each awaited acquisition for disposal or escape. RESP002 gathers origin-aware escape and flush-completion nodes, then checks whether they block every path to the read.
Analyzer validation and limits tests/Respire.Analyzers.Tests/*, docs/ANALYZER_LIMITS.md	Tests cover handler applicability, filters, gotos, generic constraints, and unsafe verification. The documentation specifies search boundaries and query limits.

Priority: ➖ Normal

Estimated code review effort: 4 (Complex) | ~50 minutes

Change: Bug fix

Sequence Diagram(s)

sequenceDiagram
  participant Analyzer
  participant ScopeWalker
  participant ReachabilityWalker
  participant FlowConditions
  participant ImplicitExceptionClassifier
  Analyzer->>ScopeWalker: Request a reachability check
  ScopeWalker->>ReachabilityWalker: Start a bounded path search
  ReachabilityWalker->>FlowConditions: Evaluate branch conditions
  FlowConditions-->>ReachabilityWalker: Return path facts
  ReachabilityWalker->>ImplicitExceptionClassifier: Classify possible implicit exceptions
  ImplicitExceptionClassifier-->>ReachabilityWalker: Return exception evidence
  ReachabilityWalker-->>ScopeWalker: Return reachability result
  ScopeWalker-->>Analyzer: Return query result

Loading

Merge Risk: ⚪ Minimal · up to 4bd1b

This change moves the disposal and pending-read analyzers to bounded, exception-aware control-flow analysis. No outstanding defects were identified, and earlier findings were addressed. Wait for CI to finish before merging.

Security Architecture Review

Security architecture risk: 🔵 Low · up to 4bd1b

The change affects compile-time warnings rather than application permissions or runtime execution. Conservative limits and explicit ownership-transfer rules constrain the risk. No introduced security vulnerability was established, but the available evidence does not establish complete proof correctness.

Retained concerns
No architecture-level concerns identified.

Security review details

Security Blast Radius

• inferred — The established exposure is analyzer execution and diagnostic outcomes for the source being analyzed. The traced paths do not establish new tenant, service, credential, or application-runtime authority.

Trust Boundaries and Controls

• observed — Source predicates feed Roslyn-based proof decisions rather than runtime authorization. Null inference rejects unstable symbols and captured values that could be stale; matching stored flush completions requires compatible reaching definitions and absence of a prior mutating call.

Resilience and Maintainability Implications

• observed — Continuation and dispatch caches are query-local, preventing reuse across different origins and barriers. Conservative exhaustion protects proof conclusions, but the documented per-query state limit is not a whole-compilation CPU or memory budget.

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 8.21% which is insufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff. Analyzed 134 functions across 12 files.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Linked Issues check	✅ Passed	[#833] The PR replaces lexical exit checks with a shared bounded, intra-scope control-flow traversal for RESP001 and RESP002. It models local jumps, exception dispatch and filters, rethrows, branch pr…
Out of Scope Changes check	✅ Passed	The traversal, exception and flow analysis, limit documentation, and analyzer regressions support [#833]. The verifier and embedded API-stub changes support those tests. The reviewed changes show no u…
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly summarizes the main change: improving analyzer exit proofs across catches, finally blocks, and local jumps.

✨ Finishing Touches 💡 1

📝 Generate docstrings 💡

• Commit to this branch
• Create a new PR

🧪 Generate unit tests (beta)

• Commit to this branch
• Create a new PR

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{A rabbit checks each branching trail,
Where handlers catch and facts prevail.
Through finally paths, the searches go,
To test what warnings should not show.
With bounded steps, the proofs stay bright,
Then hop back home beneath the moonlight.}

_{Comment @coderabbitai help to get the list of available commands.}

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-04T06:53:07.248615Z	0c776f2	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[github-actions]

Review of #847: exception-aware control-flow traversal

I read ScopeWalker.Traversal.cs in full and skimmed the diff. I did not build the PR or run its tests. The /code-review skill failed to run, so this was a manual pass. There were no earlier substantive review comments to check against.

What looks good

• The design is sound: one shared graph query used by both RESP001 and RESP002, replacing the lexical goto and exit helpers.
• Exhaustion of the 16,384-step cap returns true (a path exists), so it can't prove safety. That is the right conservative direction.
• Catches are dispatched in order, filters run before finally unwinding, and rejected filters resume the search.
• yield return is modelled as a disposal point, so a dispose after the yield no longer substitutes for a finally block.
• Resetting the known and values masks on back-edges stops one loop iteration's flush proof leaking into the next. Dropping facts can only add paths, so it errs toward warning.
• There are 23 new tests covering both positive and negative cases.

Suggestions (not bugs I could demonstrate)

1. ReachabilityWalker mixes three jobs in about 380 lines: the search loop, continuation interning, and catch-dispatch modelling (CatchDispatch, GetDispatch, Dispatch, GetCatchApplicability). Its state is a 7-field tuple pushed and popped positionally, and the _earliestEntries key is a 6-tuple. Moving exception dispatch into its own type, and replacing the state tuple with a small readonly record struct SearchState, would make argument-order mistakes harder. It would also let the dispatch rules be unit-tested without a graph search.
2. When the step cap is hit, the analyzer reports a warning with no indication that the cap was the cause. In a large method that could look like a false positive. Consider noting this in the diagnostic or the docs, or adding a test that pins the behaviour.
3. Search() rebuilds the catch-origin and unwind lists per call. That is fine at current sizes, but caching per graph would help if analysis moves to many origins per method.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b5f2fca02a

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:46:34.851Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:46:34.934Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:46:34.836Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:46:35.008Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

Review of #847

The /code-review skill failed to run, so this was a manual pass over the description, diff file list and earlier comments. I did not build the PR or run its tests.

Earlier feedback: The earlier suggestion was to replace the positional seven-field state tuple. The PR description says it is now a named SearchState with named constructor arguments, and the unused EntryPosition is gone. Traversal limits are documented in docs/ANALYZER_LIMITS.md. I did not check the head commit to confirm any of this.

Design:

• RESP001 and RESP002 now share one exception-aware graph query, replacing the lexical goto and exit helpers. That is a clear improvement.
• Hitting the 16,384-step or 64-predicate cap is treated as "a path exists", so exhaustion cannot prove safety. That is the correct conservative direction.
• Catches are dispatched in order, filters run before finally unwinding, and yield return is modelled as a disposal point.
• The 23 new positive and negative tests cover these cases.

Remaining suggestion (non-blocking): Catch dispatch is still query-local inside the walker. If it grows further, move it into its own type so the search loop stays small.

No bugs found.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 183d436f4e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[greptile-apps]

Confidence Score: 5/5

[High risk] Refactors control-flow analysis for disposal and flush checks.

The PR appears safe to merge based on this review; no outstanding finding remains.

Summary

The PR replaces lexical cleanup heuristics with bounded, exception-aware control-flow proofs shared by RESP001 and RESP002.

• Tracks acquisition and pending-read paths through branches, catches, filters, finalizers, and local jumps.
• Adds exception classification, regression coverage, and documentation of conservative analysis limits.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  A[Acquisition or pending read] --> B[Bounded control-flow search]
  B --> C{Every relevant path crosses cleanup or transfer?}
  C -- Yes --> D[Proof accepted]
  C -- No or limit reached --> E[Warning retained]

Loading

_{Reviews (91) · Last reviewed commit: "test: verify compound bitwise operand co..."}

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:55:52.513Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:55:52.582Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:55:52.705Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-03T15:55:52.589Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

Review of #847: exception-aware control-flow traversal

I reviewed this manually because the /code-review skill failed to run. I did not build the PR or run its tests.

Earlier feedback: it is addressed. The positional tuple is now a named SearchState, EntryPosition is gone, and docs/ANALYZER_LIMITS.md documents the 16,384-state and 64-predicate limits.

What looks good

• RESP001 and RESP002 now share one graph query, which replaces the lexical goto and exit helpers.
• Exhausting the traversal cap cannot prove safety, so the failure mode is a warning rather than a missed one.
• Catch ordering, filters, finally continuations and yield return are modelled.
• There are 23 new positive and negative tests.

Non-blocking suggestion: catch dispatch still lives inside the walker. Moving it into its own type would make the traversal easier to maintain, but this doesn't need to block the PR.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: a461d936cd

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

Re-review of #847 (head edfb7b4)

Manual pass: the /code-review skill failed to run. I did not build the PR or run its tests.

My earlier suggestions have been addressed:

• The seven-position tuple is now a named SearchState (ScopeWalker.Traversal.cs:29).
• The traversal limits are documented in docs/ANALYZER_LIMITS.md.
• Exhausting the step cap still cannot establish safety, which is the conservative direction.

The design is sound. RESP001 and RESP002 share one exception-aware graph query, and catch ordering, filters, finally continuations and yield return are all modelled. The PR description reports 23 new tests. The extra catch-dispatch caching I mentioned is optional and not worth blocking on.

The integration run in the PR comments shows cancelled, and a Codex review is still running. Please confirm CI is green before merging.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: edfb7b41de

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: success
• Timestamp: 2026-10-03T16:09:41.564Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:20:22.138Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:20:22.130Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:20:22.152Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:20:22.199Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

Review of #847 (exception-aware flow proofs for RESP001/RESP002)

I reviewed the PR description, the changed-file list and the earlier review comments. I could not build the project or run the tests in this environment, because the shell blocked those commands. I did not read the full diff line by line. This is a design-level review, and I'm relying on CI and the PR's reported result of 1311 passing tests for correctness.

Positives

• Replacing the duplicated lexical heuristics with one shared graph query from the actual origin is a clear architectural improvement.
• Bounding the search (<16,384 states, 64 path facts), honoring cancellation, and documenting the limits in docs/ANALYZER_LIMITS.md are the right safeguards. The limit-hit tests cover both the safe and unsafe sides.
• The earlier review follow-up (a named SearchState struct) is addressed. CodeRabbit's latest review reported no actionable comments.
• Unsafe counterparts remain covered, and expectation changes are limited to paths now proven safe.

Suggestions (non-blocking)

• The analysis is large: ScopeWalker.Traversal.cs, FlowConditions and ImplicitExceptionClassifier together. Keep a short design note in docs/ANALYZER_LIMITS.md on the invariants: what counts as a barrier, and when predicate evidence is invalidated. That would help future maintainers more than the tests alone.
• When a limit is hit, the analyzer retains the warning. Consider whether a distinct diagnostic property or message would help users tell 'proven unsafe' from 'gave up'.
• Confirm CI is green on all platforms before merging. I did not verify this.

No blocking defects found from this review.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: cb51fe0388

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:28:38.217Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:28:38.238Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:28:38.188Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:28:38.197Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

Review of #847 (exception-aware flow proofs for RESP001/RESP002)

Scope of this review: The diff is about 9,100 lines. I read the PR description, the changed-file list and the earlier review comments. I did not build the project or run the tests. I did not review the diff line by line, so I'm relying on CI and the reported 1321 passing analyzer tests for correctness.

Positives

• Replacing the duplicated lexical conditional/switch heuristics with one shared graph query from the real origin is the right direction. It removes a class of drift between RESP001 and RESP002.
• The conservative failure mode is sound. When the budget (<16,384 states, 64 path facts) runs out, the warning is kept, so a limit never produces a false proof. Both limits are documented in docs/ANALYZER_LIMITS.md and tested with safe and unsafe counterparts.
• The earlier SearchState follow-up (a named readonly IEquatable struct) is addressed.
• Expectation changes are limited to paths now proven safe, and the unsafe counterparts stay covered.

Suggestions (non-blocking)

1. Split the walker. ScopeWalker.Traversal.cs is large, and it mixes syntax-shape recognition (wrapper kinds such as tuple, cast, coalesce, with and collection expressions) with CFG registration. Moving shape recognition into a classifier, as was done for ImplicitExceptionClassifier and FlowConditions, would make each case unit-testable. It would also stop the walker growing with each new wrapper kind.
2. Document the invariants. Add a short section to docs/ANALYZER_LIMITS.md on what counts as a barrier and when predicate evidence is invalidated. That is the hardest part of this design to rediscover from the tests alone.
3. Make limit hits visible. If it is cheap, record limit-hit warnings in a diagnostic property. Users and maintainers could then tell a budget-exhausted warning from a proven-unsafe one.

None of these need to block the merge. The integration-test comments show "cancelled", which looks like a CI concurrency cancel rather than a failure. Please confirm the analyzer test job is green before merging.

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:34:45.969Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:34:45.942Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:34:45.986Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:34:45.955Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

Review of #847: exception-aware control-flow proofs for RESP001/RESP002

Scope of this review: I read the PR description, the earlier review comments, the changed-file list, docs/ANALYZER_LIMITS.md, and the file sizes and limit constants in the analyzer sources. I did not trace the traversal logic in ScopeWalker.Traversal.cs, FlowConditions.cs or ImplicitExceptionClassifier.cs line by line, and I did not build the project or run the tests. I am not claiming a full correctness audit of the 17k-line diff.

What looks good

• Replacing the duplicated lexical heuristics with one shared graph query from the real origin is the right design. RESP001 and RESP002 can no longer disagree about what counts as a safe path.
• The search is bounded: fewer than 16,384 processed states, 64 path facts, and cancellation is honored. Exhausting the fact capacity is conservative, because UnknownPathFlag can't prove a receiver non-null and an unproven barrier is dropped, which leaves more paths reachable. Failing toward a warning is the right default for an analyzer.
• docs/ANALYZER_LIMITS.md states what the proof does not cover: callee behavior after transfer, and failures of the flush or dispose itself.
• Tests include unsafe counterparts for each newly accepted safe path, and both search limits are exercised.
• The description says it follows up on earlier review feedback, for example the SearchState struct.

Suggestions

1. Size and cohesion. About 4.9k lines of analyzer code now sit in a few very large files, ScopeWalker.Traversal.cs at about 1.2k lines and PendingReadBeforeFlushAnalyzer.cs at about 1k. Consider splitting along the seams already visible in the description. The graph/reachability engine would be one piece, the predicate and correlation tracking (FlowConditions) another, and exception classification a third. Each piece would then have a narrow interface that can be unit-tested directly (as ScopeExitAnalysisTests partly does) without going through full analyzer scenarios. This is a maintainability suggestion, not a defect.
2. Hard-coded limits. MaxProcessedStates is a private const, and the doc references it by name. A test or doc check that fails when the constant and the documented number drift apart would stop the doc going stale. Alternatively, make the limit internal so the limit tests don't depend on constructing a huge input.
3. Regression visibility. Please confirm that the 1333 tests, the zero-warning build, and the CI analyzer-performance numbers are green on the final head commit. I haven't verified them myself.

Because these suggestions are open and I did not fully verify the traversal logic, I'm not marking this CLEAR. I found no concrete bug.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: d5565c53a3

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:43:52.202Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:43:52.196Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:43:52.168Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: cancelled
• Timestamp: 2026-10-04T06:43:52.227Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

Review of #847

I did not build the PR or run its tests. I read the description, the earlier review comments and the changed-file list, and I did not read the diff line by line. This PR has had about 90 prior review rounds.

Earlier feedback: The earlier suggestions are reported as addressed in the description. These are the named SearchState struct, the removal of the unused EntryPosition, and the documented limits in docs/ANALYZER_LIMITS.md. I did not check the head commit to confirm them.

Design:

• RESP001 and RESP002 now share one exception-aware graph query. This replaces duplicated lexical exit heuristics and is a clear maintainability gain.
• Hitting the 16,384-state or 64-predicate cap retains the warning, so exhaustion cannot prove safety. That is the right conservative direction.
• Both limits have safe and unsafe regression tests.
• Predicate evidence is invalidated at traversed writes, which keeps correlation proofs sound.

Non-blocking suggestion: Catch and filter dispatch modelling lives inside the walker alongside the search loop. If it grows, move it into its own type. That keeps the traversal small and lets the exception semantics be tested without driving the whole search.

No bugs found.

[github-actions]

🧪 Integration Test Results (net8.0, RESP3)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: success
• Timestamp: 2026-10-04T06:57:26.278Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP2)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: success
• Timestamp: 2026-10-04T06:57:42.203Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net8.0, RESP2)

ℹ️ Execution Details

• Framework: net8.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: success
• Timestamp: 2026-10-04T06:57:55.553Z

---

Automated integration testing with Redis containers using TUnit

[github-actions]

🧪 Integration Test Results (net10.0, RESP3)

ℹ️ Execution Details

• Framework: net10.0
• Test Runner: TUnit
• Runner: Linux - X64
• Status: success
• Timestamp: 2026-10-04T06:59:12.356Z

---

Automated integration testing with Redis containers using TUnit