Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
01 January 2008
It is well known that the use of points-to information can substantially improve the accuracy of a static program analysis. Commonly used algorithms for computing points-to information are known to be sound only for programs that have no memory errors. It thus appears impossible to utilize points-to information in an analysis of memory safety, without giving up soundness. The main result of this paper shows that a sound combination is possible, even if the points-to information is obtained independently. This result is based on a refined statement of the conditions under which a points-to analysis is sound and a general mechanism for combining conditionally sound analyses.