We present a new domain for analyzing must-equalities between address expressions. The domain is a smooth combination of Herbrand and affine equalities which enables us to describe field accesses and array indexing. While the full combination of uninterpreted functions with affine arithmetics results in intractable assertion checking algorithms, our restricted domain allows us to construct an analysis of address must-equalities that runs in polynomial time. We indicate how this analysis can be applied to infer access patterns in programs manipulating arrays and structs. © 2009 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Seidl, H., Vojdani, V., & Vene, V. (2009). A smooth combination of linear and herbrand equalities for polynomial time must-alias analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5850 LNCS, pp. 644–659). https://doi.org/10.1007/978-3-642-05089-3_41
Mendeley helps you to discover research relevant for your work.