Retaining Path-Sensitive Relations Across Control-Flow Merges

Retaining Path-Sensitive Relations Across Control-Flow Merges Douglas Gregor Sibylle Schupp We present a new value range merge operation that, unlike traditional value range merge operations, preserves arbitrary ordering relationships between program variables. We guide this new algorithm with two data structures that model interobject field relationships, enabling better precision in the analysis of object-oriented programs without prohibitive implementation or run-time costs. We discuss our own implementation of this algorithm in the STLlint static checker, which is able to verify C++ iterator loops that otherwise would require path-sensitive analysis. Department of Computer Science, Rensselaer Polytechnic Institute, Troy, NY 11/25/2003 cs-03-15

Retaining Path-Sensitive Relations Across Control-Flow Merges

Douglas Gregor

Sibylle Schupp

We present a new value range merge operation that, unlike traditional value range merge operations, preserves arbitrary ordering relationships between program variables. We guide this new algorithm with two data structures that model interobject field relationships, enabling better precision in the analysis of object-oriented programs without prohibitive implementation or run-time costs. We discuss our own implementation of this algorithm in the STLlint static checker, which is able to verify C++ iterator loops that otherwise would require path-sensitive analysis.

Department of Computer Science, Rensselaer Polytechnic Institute, Troy, NY

11/25/2003

cs-03-15