Module PointlessComparison

Simple range analysis library. Range analysis is usually done as an abstract interpretation over the lattice of range values. (A range is a pair, containing a lower and upper bound for the value.) The problem with this approach is that the lattice is very tall, which means it can take an extremely large number of iterations to find the least fixed point. This example illustrates the problem:

Provides classes and predicates for working with C/C++ code.

Holds if cmp is a comparison operation that always has the result value, and either * ss is LeftIsSmaller, and the left hand argument is always at most left, the right hand argument at least right, and left is less than or equal to right; or * ss is RightIsSmaller, and the left hand argument is always at least left, the right hand argument at most right, and left is greater than or equal to right.

Holds if cmp is a pointless comparison (see pointlessComparison above) and cmp occurs in reachable code. The reason for excluding expressions that occur in unreachable code is that range analysis sometimes can deduce impossible ranges for them. For example:

Describes which side of a pointless comparison is known to be smaller.