Pentagons: a weakly relational abstract domain for the efficient validation of array accesses