A. Simon. Splitting the Control Flow with Boolean Flags. In M. Alpuente and G. Vidal, editors, Static Analysis Symposium, volume 5079 of LNCS, pages 315-331, Valencia, Spain, July 2008. Springer.

Tools for proving the absence of run-time errors often deploy a numeric domain that approximates the possible values of a variable using linear inequalities. These abstractions are adequate since the correct program state is often convex. For instance, if the upper and lower bound of an index lie within the bounds of an array, then so do all the indices inbetween. In certain cases, for example when analysing a division operation, the correct program state is not convex. In this case correctness can be shown by splitting the control flow path, that is, by partitioning the set of execution traces which is normally implemented by analysing a path several times. We show that adding a Boolean flag to the numeric domain has the same effect. The paper discusses prerequisites, limitations and presents an improved points-to analysis using Boolean flags.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com