Fair. I suppose that even in such a scenario you shouldn't need truly global analysis to prove safety - in principle an analysis of A should reveal the soundness precondition on a safe API - though that's probably easier said than done.