Orion: High-precision methods for static error analysis of C and C++ programs
DR Dams, KS Namjoshi - Formal Methods for Components and Objects …, 2006 - Springer
Formal Methods for Components and Objects: 4th International Symposium, FMCO …, 2006•Springer
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 …
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 …
Abstract
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.
Springer