FA-11501 / Static analysis soundness / Open access

Unreachable predecessors erase definite assignments · case 01

Unreachable predecessors erase definite assignments.

Verified by executionVariant 1 · 6 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The must-analysis intersects facts from unreachable predecessors.

VERIFIED REPAIR

Intersect only reachable predecessor sets; no reachable predecessor yields None.

Unsuccessful approach: Unioning reachable predecessors admits assignments missing on another feasible path.

Case contract

Predecessors are None (unreachable) or lists of definitely assigned variables. Return their reachable intersection sorted; return None when no predecessor is reachable.

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(preds):
    if not preds: return None
    return sorted(set.intersection(*(set(p or []) for p in preds)))
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='v'+str(N)
check('dead predecessor ignored',solve([[x],None]),[x])
check('must hold on both',solve([[x,'z'],[x]]),[x])
check('reachable empty loses facts',solve([[x],[]]),[])
check('all dead',solve([None,None]),None)
check('no predecessors',solve([]),None)
check('single reachable',solve([[x]]),[x])
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
dead predecessor ignored	`[]`	`['v1']`	Failed
must hold on both	`['v1']`	`['v1']`	Passed
reachable empty loses facts	`[]`	`[]`	Passed
all dead	`[]`	`None`	Failed
no predecessors	`None`	`None`	Passed
single reachable	`['v1']`	`['v1']`	Passed

SHA-256 / ded4fffc385e675beb89ad011804bcb45c955ef9311517e0259ac97c57a4a236

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(preds):
    live=[set(p) for p in preds if p is not None]
    return sorted(set.union(*live)) if live else None
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='v'+str(N)
check('dead predecessor ignored',solve([[x],None]),[x])
check('must hold on both',solve([[x,'z'],[x]]),[x])
check('reachable empty loses facts',solve([[x],[]]),[])
check('all dead',solve([None,None]),None)
check('no predecessors',solve([]),None)
check('single reachable',solve([[x]]),[x])
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
dead predecessor ignored	`['v1']`	`['v1']`	Passed
must hold on both	`['v1', 'z']`	`['v1']`	Failed
reachable empty loses facts	`['v1']`	`[]`	Failed
all dead	`None`	`None`	Passed
no predecessors	`None`	`None`	Passed
single reachable	`['v1']`	`['v1']`	Passed

SHA-256 / 29d9a91a18ad3f936dea5be8b6f69a2b27ed87f5005115595a2b960c9fa2aa3f

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(preds):
    live=[set(p) for p in preds if p is not None]
    return sorted(set.intersection(*live)) if live else None
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='v'+str(N)
check('dead predecessor ignored',solve([[x],None]),[x])
check('must hold on both',solve([[x,'z'],[x]]),[x])
check('reachable empty loses facts',solve([[x],[]]),[])
check('all dead',solve([None,None]),None)
check('no predecessors',solve([]),None)
check('single reachable',solve([[x]]),[x])
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
dead predecessor ignored	`['v1']`	`['v1']`	Passed
must hold on both	`['v1']`	`['v1']`	Passed
reachable empty loses facts	`[]`	`[]`	Passed
all dead	`None`	`None`	Passed
no predecessors	`None`	`None`	Passed
single reachable	`['v1']`	`['v1']`	Passed

SHA-256 / 0dcd792cdf2c3918511e9a14f891607061dde34ef2cf92e45edf6258cddc33f0

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.525338+00:00.

Case digest / f43c1e3aec2e8d1f2ee55f7cae4ab2c7fe60216e9c939e28f1c6849602c9062a