Branch Reachability
branch_reachabilityAnalyze Python3 function source to determine which branches and loops are reachable, dead, or unknown, with witness inputs, using z3 without executing the code.
Instructions
Which if/elif/else arms and while/for loops of this python3 function can ever run, which are dead code, and what inputs reach each — decided with z3, without running the program.
Use trace_execution instead to see what happened on one run. Use z3_check, not this, when you already have an SMT-LIB2 script to solve directly rather than Python source to translate.
Unannotated parameters default to int. Each branch reports
verdict (reachable/dead/unknown), a witness when reachable, and
boundary_inputs (min/max/equality-edge for each comparison in its own
guard) — every input dict is shaped to drop straight into
compare_edge_cases's test_inputs. Refuses, naming the construct and
line, prior to any z3 call: floats, attribute access, comprehensions,
try/except, imports, data-dependent loop bounds, and anything else
outside + - * // %, and/or/not, == != < <= > >=, and
abs/min/max/len on int/bool/str. A for loop of at most 32
iterations is unrolled exactly; a longer for, or a while, is
checked one iteration at a time — a branch can still come back
reachable there, but never dead, and anything past the loop that
depends on what it computed comes back unknown rather than a guess.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | Python3 function source to analyze for reachable/dead branches | |
| inputs | No | Parameter name -> 'int'/'bool'/'str', to narrow or override an unannotated parameter's inferred type | |
| timeout | No | Wall-clock seconds before the z3 solver call is abandoned | |
| language | Yes | Source language of `code`; only python3 functions are analyzed | |
| max_branches | No | Max branches to analyze before stopping; default 64 |
Output Schema
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||