Abstract Domains for Bit-Level Machine Integer and Floating-point Operations

We present a few lightweight numeric abstract domains to analyze C programs that ex-ploit the binary representation of numbers in computers, for instance to perform “compute-through-overflow ” on machine integers, or to directly manipulate the exponent and man-tissa of floating-point numbers. On integers, we propose an extension of intervals with a modular component, as well as a bitfield domain. On floating-point numbers, we propose a predicate domain to match, infer, and propagate selected expression patterns. These domains are simple, efficient, and extensible. We have included them into the Astrée and AstréeA static analyzers to supplement existing domains. Experimental results show that they can improve the analysis precision at a reasonable cost.