Patent ID: 8359583
Filing Date: 2013-01-22
Classification: G06F

Abstract:
1. A method of analysis of computer program code represented by a graph structure encoded in non-transitory computer readable media; wherein the graph structure represents control flow of the computer program code; and wherein nodes of the graph represent program instructions and edges of the graph represent direction of program control flow between nodes; the method comprising: in the course of traversing each of the multiplicity of paths, producing a history in the computer readable media of each traversal that indicates code elements that correspond to nodes that exist in the program along the traversal path, wherein a respective code element may be an assignment, wherein a variable is assigned a value, and alternatively, wherein a respective code element may be an a truth decision, wherein the truth of a logical expression is evaluated as either true or false; wherein such different paths may include one or more nodes in common such that a given node may be traversed multiple times in the course of such traversals; using a checker to perform a checker analysis that produces a trigger event in response to identification of a potential defect associated with a given node in the course of a traversal of a given path that includes the given node; in response to the occurrence of the trigger event, determining whether the given node is within a false path; in response to a determination that the given node is within a false path, identifying an inconsistent combination of history elements associated with the given path, which consists of at least one of one or more assignments and/or one or more truth decisions, that results in the false path; identifying a first enabler node in the false path that makes at least one of an assignment or a truth decision within the inconsistent combination; annotating each respective merge node in the false path between the given node and the enabler node to indicate each assignment and each truth decision within the inconsistent combination that occurs within the false path between the identified first enabler node and the respective merge node; in the course of a later traversal of a different path that includes a respective annotated merge node, determining whether a history of assignments and truth decisions associated with nodes along that different path that occur at or before reaching the respective annotated merge node includes a structural match for each assignment and each truth decision indicated within the respective annotation associated with the respective annotated merge node; in response to a determination that there is a match between one or more assignments and one or more truth decisions within the history of the different path that occur at or before reaching the respective annotated merge node and each assignment and each truth decision indicated within the respective annotation associated with the respective annotated merge node, continuing traversal of the different path; and in response to a determination that there is not a match between assignments and truth decisions within the history of the different path that occur at or before reaching the respective annotated merge node and each assignment and each truth decision indicated within the respective annotation associated with the respective annotated merge node, not continuing traversal of the different path.