Apparatus and method for analyzing source code using memory operation evaluation and boolean satisfiability

A computer readable storage medium, comprising executable instructions to:

• identify a memory operation in target source code;
• develop a set of constraints associated with the memory operation, wherein the set of constraints includes base constraints derived from the target source code and additional constraints for forcing the memory operation to be out of bounds;
• convert the constraints into a Boolean expression;
• and
• process the Boolean expression with a Boolean satisfiability engine to determine whether the memory operation is potentially unsafe by executing instructions to:
• determine whether the memory operation is always safe;
• determine whether the memory operation is safe for a number of inputs if the memory operation is determined to be not always safe;
• and
• test boundary conditions for the memory operation if the memory operation is safe for at least some of the number of inputs, wherein the boundary conditions include the base constraints, constraints requiring the memory operation to be within bounds, and constraints for runtime limitations.