Reachability analysis for annotated code

We devised a reachability analysis that exploits code annotations and implemented it as a component of the extended static checker ESC/Java2. The component reports unchecked code and a class of errors previously undetected. We applied the analysis to existing annotated code and uncovered errors that were unknown to the developers. We present the algorithm performing the analysis and discuss errors that it detects.