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.