Filtering False Alarms for Static Detection of Array Bounds Violation via Weakest Precondition

Array bounds violations are a bane of programming in most languages. Static analysis provides a powerful approach to detect such bugs, but it always suffers high rate of false alarms. We propose a local, demand-driven approach based on weakest preconditions propagation to filter false alarms for static detection of array bounds violations. A concrete example is presented to show that our method is effective.