Helmut Seidl, Andrea Flexeder and Michael Petter. Interprocedurally Analysing Linear Inequality Relations. In Rocco De Nicola, editor, Programming Languages and Systems, volume 4421 of Lecture Notes in Computer Science, pages 284-299, Braga, Portugal, April 2007. Springer.
In this paper we present an alternative approach to interprocedurally inferring linear inequality relations. We propose an abstraction of the effects of procedures through convex sets of transition matrices. In the absence of conditional branching, this abstraction can be characterised precisely by means of the least solution of a constraint system. In order to handle conditionals, we introduce auxiliary variables and postpone checking them until after the procedure calls. In order to obtain an effective analysis, we approximate convex sets by means of polyhedra. Since our implementation of function composition uses the frame representation of polyhedra, we rely on the subclass of simplices to obtain an efficient implementation. We show that for this abstraction the basic operations can be implemented in polynomial time. First practical experiments indicate that the resulting analysis is quite efficient and provides reasonably precise results.
Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com