Patent ID: 7584461

Claim:
A software development method comprising: receiving a C or C++ input source file; automatically, by computer, compiling said input source file, said compiling including performing a lexical, syntactic, and semantic analysis and based at least in part on said analysis, code-generating a compiled object file comprising object code; and automatically, by computer, linking said compiled object file with system-dependent library code to produce an executable object file, wherein said semantic analysis includes employing a system of attributes of pointers, each attribute being a compile-time designation of a run-time state of an identifier, an expression, or a pointer including pointer-range states of the pointer, to infer preconditions that are applied at compile-time, at link-time, and at run-time and to infer postconditions that are applied at compile-time, at link-time, and at run-time, for at least one function within said source file, a precondition for an operation being one or more requirements imposed on preceding operations, declarations, and or initializations, and a postcondition for an operation, declaration, and initialization being one or more guarantees for subsequent operations produced by the operation, declaration, and/or initialization, maintaining a bounds data file in which requirements and guarantees are recorded for defined and undefined symbols, determining at compile-time for each operation involving pointers, arrays, and/or subscripts, whether said operation will perform in a well-defined manner without further run-time checking by determining, at compile time, whether the requirements of said operation are satisfied by the guarantees of said preceding operations, declarations, and/or initializations, wherein said code-generating produces run-time checking code sequences for operations which said determining does not determine will perform in a well-defined manner without further run-time checking, and wherein referencing said requirements and guarantees recorded in said bounds data file support said compiling, code-generating, and linking processes to automatically identify and/or eliminate within each process substantially all undefined behaviors of buffer overflow and null-pointer indirection of said input source file.