|
Abstract : |
Abstract. Symbolic Evaluation is a technique aimed at determining dynamic properties of programs. We extend our intraprocedural dataflow framework introduced in [3] to support interprocedural symbolic evaluation. Our data-flow framework utilizes a novel approach based on an array algebra to handle aliases induced by procedure calls. It serves as as a basis for static program analysis (e.g. reaching definitions-, alias analysis, worst-case performance estimations, cache analysis). Examples for reaching definitions- as well as alias analysis are presented. I Symbolic Evaluation In this section we introduce the basics of interprocedural symbolic evaluation as it is used throughout the paper. We abstract from intraprocedural evaluation details such as conditional or repetitive statements in order to be concise. Treatment of intraprocedural symbolic analysis of Ada programs can be found in [3]. Symbolic evaluation is a form of static program analysis in which symbolic expressions are used to denote the values of program variables and computations (cf. e.g. [5]). In addition a path condition describes the impact of the program's control flow onto the values of variables and the condition under which control flow reaches a given program point. The underlying program representation for symbolic evaluation is usually the control flow graph (CFG), a directed labelled graph. Its nodes are the program's basic blocks (a basic block is a single entry, single exit, sequence of statements), whereas its edges represent transfers of control between basic blocks. Each edge of the CFG is assigned a condition which must evaluate to true for the program's control flow to follow this edge. Entry and Exit are distinguished nodes used to denote start and terminal node., |
