Error Detection by Data Flow Analysis Restricted to Executable Paths

BEAM is a tool for finding errors in C++ programs by source code analysis. It uses data flow analysis to find paths leading to an error. Classical data flow analysis propagates information along all paths, including non-executable ones, which results in reporting errors that are not real. To avoid this problem, BEAM restricts data flow analysis to paths that are executable, and in addition also consistent with user’s assumptions on initial state of memory. However, the user is not required to specify his assumptions. The main contribution of this paper is an algorithm for finding an executable path to error, while avoiding path enumeration.