Interprocedural Symbolic Evaluation of Ada Programs with Aliases
Symbolic Evaluation is a technique aimed at determining dynamic properties of programs. We extend our intraprocedural data-flow framework introduced in  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.
KeywordsBasic Block Procedure Call Symbolic Expression Symbolic Evaluation Program Point
Unable to display preview. Download preview PDF.
- 1.A. V. Aho, R. Seti, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, MA, 1986.Google Scholar
- 2.J. Blieberger. Data-flow Frameworks for Worst-Case Execution Time Analysis. (submitted), 1997.Google Scholar
- 3.J. Blieberger and B. Burgstaller. Symbolic Reaching Definitions Analysis of Ada Programs. Proceedings of the Ada-Europe International Conference on Reliable Software Technologies, 238–250, June 1998.Google Scholar
- 4.J. Blieberger, T. Fahringer, and B. Scholz. An Accurate Cache Prediction for C-Programs with Symbolic Evaluation. (submitted), 1999.Google Scholar
- 6.J. D. Choi, M. Burke, and P. Carini. Efficient Flow-Sensitive Interprocedural Computation of Pointer-Induced Aliases and Side Effects. ACM PoPL, 1/93:232–245, 1993.Google Scholar
- 8.ISO/IEC 8652. Ada Reference manual, 1995.Google Scholar
- 9.W. Landi, and B. G. Ryder. Pointer-induced Aliasing: A Problem Classification. Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 235–248, 1992Google Scholar
- 11.V. C. Sreedhar. Effcient Program Analysis Using DJ Graphs. PhD thesis, School of Computer Science, McGill University, Montréal, Québec, Canada, 1995.Google Scholar