Orion: high-precision methods for static error analysis of C and C++ programs. 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.par 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.par 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.
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
- Edelkamp, Stefan; Kellershoff, Mark; Sulewski, Damian: Program model checking via action planning (2011) ioport
- Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
- Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Incremental false path elimination for static software analysis (2009)
- Dams, Dennis R.; Namjoshi, Kedar S.: Orion: high-precision methods for static error analysis of C and C++ programs (2006)