A method of formulating and solving equations that facilitate recognition of full word saturating addition and subtraction the method includes formulating, for each basis addition statement z=x+y or subtraction statement z=x y, data flow equations that describe properties of the program statements being analyzed; and solving the data flow equations. The properties may include: (a) the values bits of program variables as boolean functions of the sign bits of x, y and z; (b) the condition cond under which program statements are executed as boolean functions of the sign bits of x, y and z; and (c) the condition reach of which values of variables reach any given use of z when overflow/underflow/neither occurs. |