FA-11526 / Static analysis soundness / Open access
Unreachable input becomes an unknown constant at a join · case 01
Unreachable input becomes an unknown constant at a join.
ROOT CAUSE
Bottom (no execution) and top (any value) are collapsed into one state.
VERIFIED REPAIR
Make bottom an identity, top absorbing, and merge unequal constants to top.
Unsuccessful approach: Choosing the first non-bottom state ignores conflicting constants and later top states.
Case contract
Join constant states encoded as strings B (unreachable), T (unknown), or integer constants; return the least upper bound.
Why this case matters
A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(a, b):
return a if a==b else 'T'
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('bottom identity left',solve('B',N),N)
check('bottom identity right',solve(N,'B'),N)
check('different constants',solve(N,N+1),'T')
check('same constant',solve(N,N),N)
check('unknown absorbs right',solve(N,'T'),'T')
check('both unreachable',solve('B','B'),'B')
check('unknown absorbs left',solve('T',N),'T')
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| bottom identity left | T | 1 | Failed |
| bottom identity right | T | 1 | Failed |
| different constants | T | T | Passed |
| same constant | 1 | 1 | Passed |
| unknown absorbs right | T | T | Passed |
| both unreachable | B | B | Passed |
| unknown absorbs left | T | T | Passed |
SHA-256 / 6537eb5fc91b16f13e6f27c0074e185d6a29a9437dc7dd6dd4114186d17f1495
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(a, b):
return b if a=='B' else a
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('bottom identity left',solve('B',N),N)
check('bottom identity right',solve(N,'B'),N)
check('different constants',solve(N,N+1),'T')
check('same constant',solve(N,N),N)
check('unknown absorbs right',solve(N,'T'),'T')
check('both unreachable',solve('B','B'),'B')
check('unknown absorbs left',solve('T',N),'T')
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| bottom identity left | 1 | 1 | Passed |
| bottom identity right | 1 | 1 | Passed |
| different constants | 1 | T | Failed |
| same constant | 1 | 1 | Passed |
| unknown absorbs right | 1 | T | Failed |
| both unreachable | B | B | Passed |
| unknown absorbs left | T | T | Passed |
SHA-256 / c2d60782acf70c0db370501895d72ca4f8e5dafce8489191a286953207e0faa3
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(a, b):
if a=='B': return b
if b=='B': return a
return a if a==b else 'T'
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('bottom identity left',solve('B',N),N)
check('bottom identity right',solve(N,'B'),N)
check('different constants',solve(N,N+1),'T')
check('same constant',solve(N,N),N)
check('unknown absorbs right',solve(N,'T'),'T')
check('both unreachable',solve('B','B'),'B')
check('unknown absorbs left',solve('T',N),'T')
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| bottom identity left | 1 | 1 | Passed |
| bottom identity right | 1 | 1 | Passed |
| different constants | T | T | Passed |
| same constant | 1 | 1 | Passed |
| unknown absorbs right | T | T | Passed |
| both unreachable | B | B | Passed |
| unknown absorbs left | T | T | Passed |
SHA-256 / c3ed7825da4c8765ead7c6fecc62fe59c13e900ba5c43e56f333fd60cac44f11
Verification & scope
This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.
Observations recorded using Python 3.12.14 at 2026-09-29T14:38:48.682162+00:00.
Case digest / 8607ea59d0953b1f69a60448239289471346eb28d815b84704c2807462c6c7cd