Path-sensitive analysis framework for bug checking

Abstract

A method for performing path-sensitive data-flow analysis for use in error checking functions includes identifying at least a first instruction and a second instruction in a control flow graph of a function. The identified first instruction and second instruction are connected by at least a first control flow path and a second control flow path. The method further includes defining a path condition between the first instruction and the second instruction as a complex disjunction including a first conjunction of predicates for the first control flow path and a second conjunction of predicates for the second control flow path. The method further includes converting the path condition into conjunctive normal form to obtain a converted path condition that includes a disjunction of atomic constraints, generating a simplified path condition by simplifying the disjunction of atomic constraints in the converted path condition to a value, analyzing the function using the simplified path condition to detect an error, and presenting the error.