From assumptions to assertions: a sound and precise points-to analysis for the c language
Michael Franz, Ning Wang · 2007
Many points-to analyses for the C language only target language subsets, thereby avoiding type-unsafe features, or make assumptions in their design that input programs use type-unsafe features correctly. To overcome these simplifications, we design and implement a sound and precise points-to analysis. The complete set of assumptions needed for the soundness of an analysis are constructed during the analysis of a particular input program, and the program is instrumented with assertions to check these assumptions at run-time. Our approach offers an unambiguous design for sound points-to analysis algorithms by formalizing the assumptions made during an analysis, and integrating the assumptions and the corresponding assertions into the analysis. Our points-to analysis results in two outputs: an instrumented program that preserves the semantics of its input program, and points-to graphs that are sound with respect to the instrumented program.