Useful Abstractions: We discuss here several useful data abstractions for integer domains. Abstractions for other numeric domains can be defined similarly.
A) A Range abstraction tracks concrete values between lower and upper bounds l and u and abstracts away the rest of the values. The abstract domain is {below_l, l, …, u, above_u}.
B) The Signs abstraction is a special case of the Range abstraction where l=u=0.
C) A Set abstraction can be used instead of a Range abstraction when only equality operations are performed, as when integers are used to simulate an enumerated type. For example, a Set abstraction that tracks only the concrete values 0 and 2 will have the abstract domain {zero, two, other}.
D) A Modulo abstraction merges all integers that have the same remainder when divided by a given value.
E) The EvenOdd abstraction with abstract domain {even, odd} is a Modulo 2 abstraction.
F) Finally, the Point abstraction collapses all integer values into an abstract value unknown. This abstraction is effectively throwing away all the information about a variable, and it is useful when abstracting variables that have no significant effect on the property under analysis.