Symbolic execution of program paths involving pointer structure variables

Abstract

Many white-box testing methods are based on the analysis of program paths. For these methods, an important problem is to determine the feasibility of a given path, and find appropriate input data to execute the path if it is feasible. The symbolic execution of program paths is studied. An approach is presented, which translates a path involving pointer and structure variables to a path involving simple variables and array variables only. The later is then analyzed with constraint solving techniques. An implementation of the translation tool is described with some examples. Preliminary experimental results show that the approach is quite efficient and applicable to paths in typical programs.