We present symbolic methods to improve the precision of static analyses of modular integer expressions based on Abstract Interpretation. Like similar symbolic methods, the idea is to simplify on-the-fly arithmetic expressions before they are given to abstract transfer functions of underlying abstract domains. When manipulating fixed-length integer data types, casts and overflows generally act like modulo computations which hinder the use of symbolic techniques. The goal of this article is to formalize how modulo operations can be safely eliminated by abstracting arbitrary arithmetic expressions into sum, product, or division of linear forms with integer coefficients, while simplifying them. A common method, called “symbolic constant propagation”, enhances the simplifications of assigned variables by propagating the abstract representation of its occurrences in other expressions. Lastly, we provide some rules to simplify some expressions that are involved in the computation of linear interpolation, while ensuring the soundness of the transformation.

All these methods have been incorporated within the Astrée static analyzer that checks for the absence of run-time errors in embedded critical software.