Field-Sensitive Pointer Analysis for C Programs with Integer/Pointer Conversions

We present a field-sensitive pointer analysis algorithm for C in the presence of type conversion between integer and pointer. While field-sensitive analysis can give precise solution, it is notoriously difficult to design a correct analysis which handles all low-level dirty features of C. Most difficulties stem from arbitrary integer/pointer conversions allowed as an implementation-defined feature. To incorporate this feature into pointer analysis is not so easy as expected, and previous approaches are either unsound or greatly imprecise. In this paper, we first define the formal semantics which incorporates all low-level features of C and show that it is hardly to have precise analysis if arbitrary integer/pointer conversions are allowed. To address this, we identify the language restriction which many compiler developers implicitly assume and derive a precise analysis algorithm as an approximation of the semantics. Our analysis is shown to be sound under the restriction