×

Orion: high-precision methods for static error analysis of C and C++ programs. (English) Zbl 1196.68039

de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 4th international symposium, FMCO 2005, Amsterdam, The Netherlands, November 1–4, 2005. Revised lectures. Berlin: Springer (ISBN 3-540-36749-7/pbk). Lecture Notes in Computer Science 4111, 138-160 (2006).
Summary: We describe the algorithmic and implementation ideas behind a tool, Orion, for finding common programming errors in C and C++ programs using static code analysis. We aim to explore the fundamental trade-off between the cost and the precision of such analyses. Analysis methods that use simple dataflow domains run the risk of producing a high number of false error reports. On the other hand, the use of complex domains reduces the number of false errors, but limits the size of code that can be analyzed.
Orion employs a two-level approach: potential errors are identified by an efficient search based on a simple domain; each discovered error path is then scrutinized by a high-precision feasibility analysis aimed at filtering out as many false errors as possible.
We describe the algorithms used and their implementation in a GCC-based tool. Experimental results on a number of software programs bear out the expectation that this approach results in a high signal-to-noise ratio of reported errors, at an acceptable cost.
For the entire collection see [Zbl 1114.68010].

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX XML Cite
Full Text: DOI