Qualifying reusable functions using symbolic execution

We present an approach to reverse engineering source code modules to abstract their interface and functional specifications. A fine-grained program representation for C programs, the Combined C Graph (CGG), is used to perform dynamic analysis of a module by means of symbolic execution techniques. We focus on problems like pointer variables and expressions containing embedded side-effects and control flows. The role of the user interaction to understand the module behaviour and to deal with invariant assertions is also discussed. The functional specifications are produced in the form of first order logic formulas called preconditions and postconditions.