Automated safe secure techniques for eliminating undefined behavior in computer software

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.